A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

Christoph Lange; Marco B. Caminati; Manfred Kerber; Till Mossakowski; Colin Rowat; Makarius Wenzel; Wolfgang Windsteiger

doi:10.1007/978-3-642-39320-4_13

A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

Christoph Lange
, Marco B. Caminati
, Manfred Kerber
, Till Mossakowski
, Colin Rowat
, Makarius Wenzel
, Wolfgang Windsteiger

Research Institute for Symbolic Computation

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new design has the desired properties, such as efficiency, i.e. allocating goods to those bidders who value them most? We say: by formal, machine-checked proofs. We investigated the suitability of the Isabelle, Theorema, Mizar, and Hets/CASL/TPTP theorem provers for reproducing a key result of auction theory: Vickrey's 1961 theorem on the properties of second-price auctions. Based on our formalisation experience, taking an auction designer's perspective, we give recommendations on what system to use for formalising auctions, and outline further steps towards a complete auction theory toolbox.

Original language	English
Title of host publication	Conference on Intelligent Computer Mathematics (CICM 2013)
Editors	Jacques Carette
Publisher	Springer
Pages	200-215
Number of pages	16
Volume	7961
ISBN (Print)	9783642393198
DOIs	https://doi.org/10.1007/978-3-642-39320-4_13
Publication status	Published - 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7961 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Fields of science

101001 Algebra
101002 Analysis
101 Mathematics
102 Computer Sciences
102011 Formal languages
101009 Geometry
101013 Mathematical logic
101020 Technical mathematics
101025 Number theory
101012 Combinatorics
101005 Computer algebra
101006 Differential geometry
101003 Applied geometry
102025 Distributed systems

JKU Focus areas

Computation in Informatics and Mathematics

Access to Document

10.1007/978-3-642-39320-4_13

Cite this

Lange, C., Caminati, M. B., Kerber, M., Mossakowski, T., Rowat, C., Wenzel, M., & Windsteiger, W. (2013). A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. In Jacques Carette (Ed.), Conference on Intelligent Computer Mathematics (CICM 2013) (Vol. 7961, pp. 200-215). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7961 LNAI). Springer. https://doi.org/10.1007/978-3-642-39320-4_13

Lange, Christoph ; Caminati, Marco B. ; Kerber, Manfred et al. / A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. Conference on Intelligent Computer Mathematics (CICM 2013). editor / Jacques Carette. Vol. 7961 Springer, 2013. pp. 200-215 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{5e65116808154a679ece1aaf3530736e,

title = "A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory",

abstract = "Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new design has the desired properties, such as efficiency, i.e. allocating goods to those bidders who value them most? We say: by formal, machine-checked proofs. We investigated the suitability of the Isabelle, Theorema, Mizar, and Hets/CASL/TPTP theorem provers for reproducing a key result of auction theory: Vickrey's 1961 theorem on the properties of second-price auctions. Based on our formalisation experience, taking an auction designer's perspective, we give recommendations on what system to use for formalising auctions, and outline further steps towards a complete auction theory toolbox.",

author = "Christoph Lange and Caminati, \{Marco B.\} and Manfred Kerber and Till Mossakowski and Colin Rowat and Makarius Wenzel and Wolfgang Windsteiger",

year = "2013",

doi = "10.1007/978-3-642-39320-4\_13",

language = "English",

isbn = "9783642393198",

volume = "7961",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "200--215",

editor = "\{Jacques Carette\}",

booktitle = "Conference on Intelligent Computer Mathematics (CICM 2013)",

}

Lange, C, Caminati, MB, Kerber, M, Mossakowski, T, Rowat, C, Wenzel, M & Windsteiger, W 2013, A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. in Jacques Carette (ed.), Conference on Intelligent Computer Mathematics (CICM 2013). vol. 7961, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7961 LNAI, Springer, pp. 200-215. https://doi.org/10.1007/978-3-642-39320-4_13

A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. / Lange, Christoph; Caminati, Marco B.; Kerber, Manfred et al.
Conference on Intelligent Computer Mathematics (CICM 2013). ed. / Jacques Carette. Vol. 7961 Springer, 2013. p. 200-215 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7961 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

AU - Lange, Christoph

AU - Caminati, Marco B.

AU - Kerber, Manfred

AU - Mossakowski, Till

AU - Rowat, Colin

AU - Wenzel, Makarius

AU - Windsteiger, Wolfgang

PY - 2013

Y1 - 2013

N2 - Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new design has the desired properties, such as efficiency, i.e. allocating goods to those bidders who value them most? We say: by formal, machine-checked proofs. We investigated the suitability of the Isabelle, Theorema, Mizar, and Hets/CASL/TPTP theorem provers for reproducing a key result of auction theory: Vickrey's 1961 theorem on the properties of second-price auctions. Based on our formalisation experience, taking an auction designer's perspective, we give recommendations on what system to use for formalising auctions, and outline further steps towards a complete auction theory toolbox.

AB - Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new design has the desired properties, such as efficiency, i.e. allocating goods to those bidders who value them most? We say: by formal, machine-checked proofs. We investigated the suitability of the Isabelle, Theorema, Mizar, and Hets/CASL/TPTP theorem provers for reproducing a key result of auction theory: Vickrey's 1961 theorem on the properties of second-price auctions. Based on our formalisation experience, taking an auction designer's perspective, we give recommendations on what system to use for formalising auctions, and outline further steps towards a complete auction theory toolbox.

UR - https://www.scopus.com/pages/publications/84880760011

U2 - 10.1007/978-3-642-39320-4_13

DO - 10.1007/978-3-642-39320-4_13

M3 - Conference proceedings

SN - 9783642393198

VL - 7961

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 200

EP - 215

BT - Conference on Intelligent Computer Mathematics (CICM 2013)

A2 - Jacques Carette, null

PB - Springer

ER -

Lange C, Caminati MB, Kerber M, Mossakowski T, Rowat C, Wenzel M et al. A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. In Jacques Carette, editor, Conference on Intelligent Computer Mathematics (CICM 2013). Vol. 7961. Springer. 2013. p. 200-215. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-39320-4_13

A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory

Abstract

Publication series

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cite this