# Budget imbalance criteria for auctions: A formalized theorem

Research output: Contribution to conference (unpublished) › Paper › peer-review

## Standard

**Budget imbalance criteria for auctions: A formalized theorem.** / Caminati, Marco B.; Kerber, Manfred; Rowat, Colin.

Research output: Contribution to conference (unpublished) › Paper › peer-review

## Harvard

## APA

*Budget imbalance criteria for auctions: A formalized theorem*. 35-44. Paper presented at Trends in Contemporary Computer Science, Białystok, Poland. http://alioth.uwb.edu.pl/~mml/6pcm/ComputerScience/Monograph-ComputerSciencePodlasie2014.pdf

## Vancouver

## Author

## Bibtex

}

## RIS

TY - CONF

T1 - Budget imbalance criteria for auctions: A formalized theorem

AU - Caminati, Marco B.

AU - Kerber, Manfred

AU - Rowat, Colin

N1 - ISBN 978-83-62582-58-7

PY - 2014/7/1

Y1 - 2014/7/1

N2 - We present an original theorem in auction theory: it specifiesgeneral conditions under which the sum of the payments of all bidders isnecessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theoremapplies to the important case of a second-price Vickrey auction, where itreduces to a basic result of which a novel proof is given. To enhance theconfidence in this new theorem, it has been formalized in Isabelle/HOL:the main results and definitions of the formal proof are reproduced herein common mathematical language, and are accompanied by an informaldiscussion about the underlying ideas.

AB - We present an original theorem in auction theory: it specifiesgeneral conditions under which the sum of the payments of all bidders isnecessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theoremapplies to the important case of a second-price Vickrey auction, where itreduces to a basic result of which a novel proof is given. To enhance theconfidence in this new theorem, it has been formalized in Isabelle/HOL:the main results and definitions of the formal proof are reproduced herein common mathematical language, and are accompanied by an informaldiscussion about the underlying ideas.

M3 - Paper

SP - 35

EP - 44

T2 - Trends in Contemporary Computer Science

Y2 - 1 July 2014 through 4 July 2014

ER -