zbMATH — the first resource for mathematics

A qualitative comparison of the suitability of four theorem provers for basic auction theory. (English) Zbl 1390.68577
Carette, Jacques (ed.) et al., Intelligent computer mathematics. MKM, Calculemus, DML, and systems and projects 2013, held as part of CICM 2013, Bath, UK, July 8–12, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-39319-8/pbk). Lecture Notes in Computer Science 7961. Lecture Notes in Artificial Intelligence, 200-215 (2013).
Summary: 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.
For the entire collection see [Zbl 1268.68008].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
91-04 Software, source code, etc. for problems pertaining to game theory, economics, and finance
91B26 Auctions, bargaining, bidding and selling, and other market models
Full Text: DOI