Universität Bremen  
  FB 3  
  Group BKB > Publications > Search > Deutsch

Publications Search - Details

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

 Back to result list
Author: Automatically generated page
  Group BKB 
Last updated: February 23, 2006   impressum