A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory
复制标题
四个定理证明者对基本拍卖理论适用性的定性比较
DOI：
10.1007/978-3-642-39320-4_13
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
W. Windsteiger
中科院分区：
文献类型：
--
作者：
C. Lange;M. Caminati;Manfred Kerber;Till Mossakowski;C. Rowat;M. Wenzel;W. Windsteiger
新颖的拍卖方案不断被设计出来。它们的设计对商品的分配和产生的收入具有重大影响。但是如何判断新设计是否具有所需的属性，例如效率，即将商品分配给最看重它们的投标人？我们说：通过正式的、机器检查的证明。我们研究了 Isabelle、Theorema、Mizar 和 Hets/CASL/TPTP 定理证明者再现拍卖理论关键结果的适用性：Vickrey 1961 年关于二价拍卖属性的定理。根据我们的形式化经验，从拍卖设计者的角度，我们就使用什么系统进行形式化拍卖提出建议，并概述了实现完整拍卖理论工具箱的进一步步骤。
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.