Standard
A qualitative comparison of the suitability of four theorem provers for basic auction theory. / Lange, Christoph
; Caminati, Marco B; Kerber, Manfred et al.
Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings 6. Vol. 7961 Springer, 2013. p. 200-215.
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review
Harvard
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
Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings 6. vol. 7961, Springer, pp. 200-215.
https://doi.org/10.1007/978-3-642-39320-4_13APA
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
Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings 6 (Vol. 7961, pp. 200-215). Springer.
https://doi.org/10.1007/978-3-642-39320-4_13Vancouver
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 Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings 6. Vol. 7961. Springer. 2013. p. 200-215 doi: 10.1007/978-3-642-39320-4_13
Author
Lange, Christoph
; Caminati, Marco B ; Kerber, Manfred et al. /
A qualitative comparison of the suitability of four theorem provers for basic auction theory. Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings 6. Vol. 7961 Springer, 2013. pp. 200-215
Bibtex
@inproceedings{5eef4566389943af8513e384542f107a,
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 Caminati, {Marco B} and Manfred Kerber and Till Mossakowski and Colin Rowat and Makarius Wenzel and Wolfgang Windsteiger",
year = "2013",
month = jul,
day = "1",
doi = "10.1007/978-3-642-39320-4_13",
language = "English",
isbn = "978-3-642-39319-8",
volume = "7961",
pages = "200--215",
booktitle = "Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings 6",
publisher = "Springer",
}
RIS
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/7/1
Y1 - 2013/7/1
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.
U2 - 10.1007/978-3-642-39320-4_13
DO - 10.1007/978-3-642-39320-4_13
M3 - Conference contribution/Paper
SN - 978-3-642-39319-8
VL - 7961
SP - 200
EP - 215
BT - Intelligent Computer Mathematics: MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings 6
PB - Springer
ER -
