@inproceedings{LangeEtAl13,
  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.},
  added-at = {2016-08-05T15:59:03.000+0200},
  author = {Lange, Christoph and Caminati, Marco B. and Kerber, Manfred and Mossakowski, Till and Rowat, Colin and Wenzel, Makarius and Windsteiger, Wolfgang},
  biburl = {https://www.bibsonomy.org/bibtex/2400437942fc806cbdfa66ec3d577c0c7/tillmo},
  booktitle = {Intelligent Computer Mathematics, Conferences on Intelligent Computer Mathematics},
  editor = {Carette, Jacques and Davenport, James H. and Windsteiger, Wolfgang and Sojka, Petr and Aspinall, David and Lange, Christoph},
  interhash = {04efea7c104cdd7b72f7a82bf7c4a86f},
  intrahash = {400437942fc806cbdfa66ec3d577c0c7},
  keywords = {CASL Hets Isabelle Mizar TPTP Theorema auction comparison proving theorem},
  pages = {200--215},
  pdfurl = {http://www.informatik.uni-bremen.de/~till/papers/auction-prover-comparison.pdf},
  publisher = {Springer-Verlag Berlin Heidelberg},
  series = {Lecture Notes in Computer Science},
  status = {Reviewed},
  timestamp = {2016-08-05T15:59:03.000+0200},
  title = {A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory},
  url = {http://link.springer.com/chapter/10.1007%2F978-3-642-39320-4_13},
  volume = 7961,
  year = 2013
}