2013/03/18 by Christoph Lange, Marco B. Caminati, Lange, Christoph +11
Computer Science · #03B10 #03B15 #03B35 #03B70 #68T15 #68T35 #91B26 #Computer Science and Game Theory (cs.GT) #F.4.1 #FOS: Computer and information sciences #H.1.2 #I.2.3 #I.2.4 #J.4 #Logic in Computer Science (cs.LO) #Mathematical Software (cs.MS) #acm:03B10 #acm:03B15 #acm:03B35 #acm:03B70 #acm:68T15 #acm:68T35 #acm:91B26 #cs.GT #cs.LO #cs.MS #msc:03B10 #msc:03B15 #msc:03B35 #msc:03B70 #msc:68T15 #msc:68T35 #msc:91B26
paper · pdf · doi:10.48550/arxiv.1303.4193
Conference on Intelligent Computer Mathematics, 8-12 July, Bath, UK. Published as number 7961 in Lecture Notes in Artificial Intelligence, Springer
arxiv created 2013/05/23 · arxiv updated 2013/05/24
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.