%0 Conference Paper %1 LangeEtAl13 %A Lange, Christoph %A Caminati, Marco B. %A Kerber, Manfred %A Mossakowski, Till %A Rowat, Colin %A Wenzel, Makarius %A Windsteiger, Wolfgang %B Intelligent Computer Mathematics, Conferences on Intelligent Computer Mathematics %D 2013 %E Carette, Jacques %E Davenport, James H. %E Windsteiger, Wolfgang %E Sojka, Petr %E Aspinall, David %E Lange, Christoph %I Springer-Verlag Berlin Heidelberg %K CASL Hets Isabelle Mizar TPTP Theorema auction comparison proving theorem %P 200--215 %T A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory %U http://link.springer.com/chapter/10.1007%2F978-3-642-39320-4_13 %V 7961 %X 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.

@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 }