A qualitative comparison of the suitability of four theorem provers for basic auction theory
CICM'13 Proceedings of the 2013 international conference on Intelligent Computer Mathematics(2013)
摘要
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.
更多查看译文
关键词
complete auction theory toolbox,qualitative comparison,basic auction theory,auction theory,auction designer,key result,formalisation experience,novel auction scheme,formalising auction,tptp theorem provers,second-price auction,new design
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要