Budget imbalance criteria for auctions: A formalized theorem

Research output: Contribution to conference (unpublished)Paper

Colleges, School and Institutes

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.

Bibliographic note

ISBN 978-83-62582-58-7

Details

Original languageEnglish
Pages35-44
Number of pages10
Publication statusPublished - 1 Jul 2014
EventTrends in Contemporary Computer Science - http://katmat.pb.bialystok.pl/pcm14/programy/program_detailed_v2.pdf, Białystok, Poland
Duration: 1 Jul 20144 Jul 2014

Conference

ConferenceTrends in Contemporary Computer Science
CountryPoland
CityBiałystok
Period1/07/144/07/14