Budget Imbalance Criteria for Auctions: A Formalized Theorem
We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily 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 theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.
Year of publication: |
2014-11
|
---|---|
Authors: | Caminati, Marco B. ; Kerber, Manfred ; Rowat, Colin |
Institutions: | arXiv.org |
Saved in:
freely available
Saved in favorites
Similar items by person
-
Sound auction specification and implementation
Caminati, Marco B., (2015)
-
Sound Auction Specification and Implementation
Caminati, Marco B, (2015)
-
A Ramsey bound on stable sets in Jordan pillage games
Kerber, Manfred, (2011)
- More ...