RISC RISC Research Institute for Symbolic Computation  
  • @inproceedings{RISC4723,
    author = {Christoph Lange and Marco B. Caminati and Manfred Kerber and Till Mossakowski and Colin Rowat and Makarius Wenzel and Wolfgang Windsteiger},
    title = {{A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory}},
    booktitle = {{Conference on Intelligent Computer Mathematics (CICM 2013)}},
    language = {english},
    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.},
    series = {Lecture Notes in Artificial Intelligence (LNAI)},
    volume = {7961},
    pages = {200--215},
    publisher = {Springer},
    isbn_issn = {ISBN 978-3-642-39319-8},
    year = {2013},
    editor = {Jacques Carette},
    refereed = {yes},
    length = {16}