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

Christoph Lange; Marco 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 Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

9 Citations (Scopus)

252 Downloads (Pure)

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	Intelligent Computer Mathematics
Editors	Jacques Carette, James Davenport, Wolfgang Windsteiger, Petr Sojka, David Aspinall, Christoph Lange
Publisher	Springer
Pages	200-215
Volume	7961
ISBN (Electronic)	978-3-642-39320-4
ISBN (Print)	978-3-642-39319-8
DOIs	https://doi.org/10.1007/978-3-642-39320-4_13
Publication status	Published - 2013
Event	Conferences on Intelligent Computer Mathematics - Bath, United Kingdom Duration: 8 Jul 2013 → 12 Jul 2013

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	7961
ISSN (Print)	0302-9743

Conference

Conference	Conferences on Intelligent Computer Mathematics
Country/Territory	United Kingdom
City	Bath
Period	8/07/13 → 12/07/13

Access to Document

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

Lange_et_al_Qualitative_Comparison_Four_Theorem_Provers_2013
The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-642-39320-4_13
Accepted author manuscript, 199 KBLicence: None: All rights reserved

Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour
Kerber, M. & Rowat, C.
Engineering & Physical Science Research Council
1/05/12 → 30/04/15
Project: Research Councils

Cite this

Lange, C., Caminati, M., 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 J. Carette, J. Davenport, W. Windsteiger, P. Sojka, D. Aspinall, & C. Lange (Eds.), Intelligent Computer Mathematics (Vol. 7961, pp. 200-215). (Lecture Notes in Computer Science; Vol. 7961). Springer. https://doi.org/10.1007/978-3-642-39320-4_13

Lange, Christoph ; Caminati, Marco ; Kerber, Manfred et al. / A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. Intelligent Computer Mathematics. editor / Jacques Carette ; James Davenport ; Wolfgang Windsteiger ; Petr Sojka ; David Aspinall ; Christoph Lange. Vol. 7961 Springer, 2013. pp. 200-215 (Lecture Notes in Computer Science).

@inproceedings{12bfd02400904a39a9c45e42c5dfadc7,

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{\textquoteright}s 1961 theorem on the properties of second-price auctions. Based on our formalisation experience, taking an auction designer{\textquoteright}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 Marco Caminati 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 = "978-3-642-39319-8",

volume = "7961",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "200--215",

editor = "Jacques Carette and James Davenport and Wolfgang Windsteiger and Petr Sojka and David Aspinall and Christoph Lange",

booktitle = "Intelligent Computer Mathematics",

note = "Conferences on Intelligent Computer Mathematics ; Conference date: 08-07-2013 Through 12-07-2013",

}

Lange, C, Caminati, M, 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 J Carette, J Davenport, W Windsteiger, P Sojka, D Aspinall & C Lange (eds), Intelligent Computer Mathematics. vol. 7961, Lecture Notes in Computer Science, vol. 7961, Springer, pp. 200-215, Conferences on Intelligent Computer Mathematics, Bath, United Kingdom, 8/07/13. 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; Kerber, Manfred et al.
Intelligent Computer Mathematics. ed. / Jacques Carette; James Davenport; Wolfgang Windsteiger; Petr Sojka; David Aspinall; Christoph Lange. Vol. 7961 Springer, 2013. p. 200-215 (Lecture Notes in Computer Science; Vol. 7961).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

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

AU - Lange, Christoph

AU - Caminati, Marco

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 - http://arxiv.org/abs/1303.4193

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

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

M3 - Conference contribution

SN - 978-3-642-39319-8

VL - 7961

T3 - Lecture Notes in Computer Science

SP - 200

EP - 215

BT - Intelligent Computer Mathematics

A2 - Carette, Jacques

A2 - Davenport, James

A2 - Windsteiger, Wolfgang

A2 - Sojka, Petr

A2 - Aspinall, David

A2 - Lange, Christoph

PB - Springer

T2 - Conferences on Intelligent Computer Mathematics

Y2 - 8 July 2013 through 12 July 2013

ER -

Lange C, Caminati M, 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 Carette J, Davenport J, Windsteiger W, Sojka P, Aspinall D, Lange C, editors, Intelligent Computer Mathematics. Vol. 7961. Springer. 2013. p. 200-215. (Lecture Notes in Computer Science). 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

Conference

Access to Document

Projects

Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour

Cite this