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 proceedingConference contribution

9 Citations (Scopus)
237 Downloads (Pure)


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 languageEnglish
Title of host publicationIntelligent Computer Mathematics
EditorsJacques Carette, James Davenport, Wolfgang Windsteiger, Petr Sojka, David Aspinall, Christoph Lange
ISBN (Electronic)978-3-642-39320-4
ISBN (Print)978-3-642-39319-8
Publication statusPublished - 2013
EventConferences on Intelligent Computer Mathematics - Bath, United Kingdom
Duration: 8 Jul 201312 Jul 2013

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


ConferenceConferences on Intelligent Computer Mathematics
Country/TerritoryUnited Kingdom

Cite this