| Publication type: |
Article in Proceedings |
| Author: |
Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger |
| Editor: |
Jacques Carette, James H. Davenport, Wolfgang Windsteiger, Petr Sojka, David Aspinall, Christoph Lange |
| Title: |
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory |
| Book / Collection title: |
Intelligent Computer Mathematics, Conferences on Intelligent Computer Mathematics |
| Volume: |
7961 |
| Page(s): |
200 – 215 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2013 |
| Publisher: |
Springer-Verlag Berlin Heidelberg |
| 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. |
| Internet: |
http://link.springer.com/chapter/10.1007%2F978-3-642-39320-4_13 |
| PDF Version: |
http://www.informatik.uni-bremen.de/~till/papers/auction-prover-comparison.pdf |
| Keywords: |
auction CASL Hets TPTP Isabelle Theorema Mizar theorem proving comparison |
| Status: |
Reviewed |
| Last updated: |
17. 01. 2014 |
|
 |
