Abstract
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 reproduced here
in common mathematical language, and are accompanied by an informal
discussion about the underlying ideas.
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 reproduced here
in common mathematical language, and are accompanied by an informal
discussion about the underlying ideas.
| Original language | English |
|---|---|
| Pages | 35-44 |
| Number of pages | 10 |
| Publication status | Published - 1 Jul 2014 |
| Event | Trends in Contemporary Computer Science - http://katmat.pb.bialystok.pl/pcm14/programy/program_detailed_v2.pdf, Białystok, Poland Duration: 1 Jul 2014 → 4 Jul 2014 |
Conference
| Conference | Trends in Contemporary Computer Science |
|---|---|
| Country/Territory | Poland |
| City | Białystok |
| Period | 1/07/14 → 4/07/14 |