| Art der Veröffentlichung: |
Artikel in Konferenzband |
| Autor: |
Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, Wolfgang Windsteiger |
| Herausgeber: |
Jacques Carette, James H. Davenport, Wolfgang Windsteiger, Petr Sojka, David Aspinall, Christoph Lange |
| Titel: |
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory |
| Buch / Sammlungs-Titel: |
Intelligent Computer Mathematics, Conferences on Intelligent Computer Mathematics |
| Band: |
7961 |
| Seite(n): |
200 – 215 |
| Serie / Reihe: |
Lecture Notes in Computer Science |
| Erscheinungsjahr: |
2013 |
| Verleger: |
Springer-Verlag Berlin Heidelberg |
| Abstract / Kurzbeschreibung: |
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 |
| Schlagworte: |
auction CASL Hets TPTP Isabelle Theorema Mizar theorem proving comparison |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
17. 01. 2014 |
