四种定理证明器在基础拍卖理论中适用性的定性比较
计算机科学中的逻辑
2013-05-24 v3 计算机科学与博弈论
数学软件
摘要
新的拍卖方案不断被设计出来。其设计对商品分配和产生的收入有重大影响。但如何判断一个新设计是否具有期望的性质，例如效率（即将商品分配给那些最看重它们的竞拍者）？我们提出：通过形式化的、机器验证的证明。我们研究了Isabelle、Theorema、Mizar和Hets/CASL/TPTP定理证明器在复现拍卖理论的一个关键结果——维克里1961年关于第二价格拍卖性质的定理——方面的适用性。基于我们的形式化经验，从拍卖设计者的角度，我们给出了关于使用哪个系统来形式化拍卖的建议，并概述了迈向完整拍卖理论工具箱的进一步步骤。
引用
@article{arxiv.1303.4193,
title = {A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory},
author = {Christoph Lange and Marco B. Caminati and Manfred Kerber and Till Mossakowski and Colin Rowat and Makarius Wenzel and Wolfgang Windsteiger},
journal= {arXiv preprint arXiv:1303.4193},
year = {2013}
}
备注
Conference on Intelligent Computer Mathematics, 8-12 July, Bath, UK. Published as number 7961 in Lecture Notes in Artificial Intelligence, Springer