Sound Auction Specification and Implementation
Sound Auction Specification and Implementation
复制标题
完善的拍卖规范和实施
DOI：
10.1145/2764468.2764511
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Caminati M
中科院分区：
文献类型：
--
作者：
Caminati M
我们从计算机科学中引入了机械化推理的“形式化方法”，以解决拍卖设计和实践中的两个问题：给定的拍卖设计是否被充分指定，拥有其预期的属性；当实际运行时，设计是否被忠实地实现？在大型拍卖中，任何一方失败都可能付出巨大代价。在熟悉的组合Vickrey拍卖设置中，我们使用一个机械化推理器Isabelle，首先确保拍卖具有一组所需的属性（例如，以非负价格分配所有物品），然后直接从指定的设计生成经过验证的可执行代码。在已知的环境中建立预期的结果之后，我们打算下一步使用正式的方法来验证新的拍卖设计。
We introduce `formal methods' of mechanized reasoning from computer science to address two problems in auction design and practice: is a given auction design soundly specified, possessing its intended properties; and, is the design faithfully implemented when actually run? Failure on either front can be hugely costly in large auctions. In the familiar setting of the combinatorial Vickrey auction, we use a mechanized reasoner, Isabelle, to first ensure that the auction has a set of desired properties (e.g. allocating all items at non-negative prices), and to then generate verified executable code directly from the specified design. Having established the expected results in a known context, we intend next to use formal methods to verify new auction designs.
登录
查看更多内容
通用 Tableau Prover 及其与 Isabelle 的集成
DOI：
10.3217/jucs-005-03-0073
发表时间：
1999
期刊：
J. Univers. Comput. Sci.
影响因子：
--
作者：
Lawrence Charles Paulson
通讯作者：
Lawrence Charles Paulson
影响因子：
0.9
作者：
J. Harrison
通讯作者：
J. Harrison
DOI：
10.1007/978-3-540-93920-7_13
发表时间：
2008
期刊：
Eng. Appl. Artif. Intell.
影响因子：
--
作者：
E. Tadjouddine;Frank Guerin;W. Vasconcelos
通讯作者：
W. Vasconcelos
组合拍卖的测试套件
DOI：
10.7551/mitpress/9780262033428.003.0019
发表时间：
2005
期刊：
Eng. Appl. Artif. Intell.
影响因子：
--
作者：
Kevin Leyton;Y. Shoham
通讯作者：
Y. Shoham
四个定理证明者对基本拍卖理论适用性的定性比较
DOI：
10.1007/978-3-642-39320-4_13
发表时间：
2013
期刊：
arXiv: Metric Geometry
影响因子：
--
作者：
C. Lange;M. Caminati;Manfred Kerber;Till Mossakowski;C. Rowat;M. Wenzel;W. Windsteiger
通讯作者：
W. Windsteiger