Budget imbalance criteria for auctions: A formalized theorem

Research output: Contribution to conference (unpublished)Paperpeer-review

Standard

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

2014. 35-44 Paper presented at Trends in Contemporary Computer Science, Białystok, Poland.

Research output: Contribution to conference (unpublished)Paperpeer-review

Harvard

APA

Vancouver

Caminati MB, Kerber M, Rowat C. Budget imbalance criteria for auctions: A formalized theorem. 2014. Paper presented at Trends in Contemporary Computer Science, Białystok, Poland.

Author

Caminati, Marco B. ; Kerber, Manfred ; Rowat, Colin. / Budget imbalance criteria for auctions: A formalized theorem. Paper presented at Trends in Contemporary Computer Science, Białystok, Poland.10 p.

Bibtex

@conference{071381506c5142b6b771098c0144e033,
title = "Budget imbalance criteria for auctions: A formalized theorem",
abstract = "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.",
author = "Caminati, {Marco B.} and Manfred Kerber and Colin Rowat",
note = "ISBN 978-83-62582-58-7; Trends in Contemporary Computer Science ; Conference date: 01-07-2014 Through 04-07-2014",
year = "2014",
month = jul,
day = "1",
language = "English",
pages = "35--44",

}

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 -