英文标题：
《Budget Imbalance Criteria for Auctions: A Formalized Theorem》
---
作者：
Marco B. Caminati, Manfred Kerber, Colin Rowat
---
最新提交年份：
2014
---
英文摘要：
We present an original theorem in auction theory: it specifies general conditions under which the sum of the payments of all bidders is necessarily not identically zero, and more generally not constant. Moreover, it explicitly supplies a construction for a finite minimal set of possible bids on which such a sum is not constant. In particular, this theorem applies to the important case of a second-price Vickrey auction, where it reduces to a basic result of which a novel proof is given. To enhance the confidence in this new theorem, it has been formalized in Isabelle/HOL: the main results and definitions of the formal proof are re- produced here in common mathematical language, and are accompanied by an informal discussion about the underlying ideas.
---
中文摘要：
我们在拍卖理论中提出了一个原始定理：它规定了一般条件，在此条件下，所有投标人的付款总额不一定为零，更一般地说，也不是常数。此外，它显式地提供了一个有限最小可能出价集的构造，在这个集合上，这样的总和不是常数。特别地，这个定理适用于第二价格Vickrey拍卖的重要情况，在这种情况下，它归结为一个基本结果，并给出了一个新的证明。为了增强对这个新定理的信心，它在Isabelle/HOL中被形式化：这里用通用数学语言重新生成了形式证明的主要结果和定义，并伴随着关于基本思想的非正式讨论。
---
分类信息：

一级分类：Quantitative Finance 数量金融学
二级分类：Mathematical Finance 数学金融学
分类描述：Mathematical and analytical methods of finance, including stochastic, probabilistic and functional analysis, algebraic, geometric and other methods
金融的数学和分析方法，包括随机、概率和泛函分析、代数、几何和其他方法
--
一级分类：Computer Science 计算机科学
二级分类：Computer Science and Game Theory 计算机科学与博弈论
分类描述：Covers all theoretical and applied aspects at the intersection of computer science and game theory, including work in mechanism design, learning in games (which may overlap with Learning), foundations of agent modeling in games (which may overlap with Multiagent systems), coordination, specification and formal methods for non-cooperative computational environments. The area also deals with applications of game theory to areas such as electronic commerce.
涵盖计算机科学和博弈论交叉的所有理论和应用方面，包括机制设计的工作，游戏中的学习（可能与学习重叠），游戏中的agent建模的基础（可能与多agent系统重叠），非合作计算环境的协调、规范和形式化方法。该领域还涉及博弈论在电子商务等领域的应用。
--
一级分类：Computer Science 计算机科学
二级分类：Logic in Computer Science 计算机科学中的逻辑
分类描述：Covers all aspects of logic in computer science, including finite model theory, logics of programs, modal logic, and program verification. Programming language semantics should have Programming Languages as the primary subject area. Roughly includes material in ACM Subject Classes D.2.4, F.3.1, F.4.0, F.4.1, and F.4.2; some material in F.4.3 (formal languages) may also be appropriate here, although Computational Complexity is typically the more appropriate subject area.
涵盖计算机科学中逻辑的所有方面，包括有限模型理论，程序逻辑，模态逻辑和程序验证。程序设计语言语义学应该把程序设计语言作为主要的学科领域。大致包括ACM学科类D.2.4、F.3.1、F.4.0、F.4.1和F.4.2中的材料；F.4.3（形式语言）中的一些材料在这里也可能是合适的，尽管计算复杂性通常是更合适的主题领域。
--
一级分类：Quantitative Finance 数量金融学
二级分类：Economics 经济学
分类描述：q-fin.EC is an alias for econ.GN. Economics, including micro and macro economics, international economics, theory of the firm, labor economics, and other economic topics outside finance
q-fin.ec是econ.gn的别名。经济学，包括微观和宏观经济学、国际经济学、企业理论、劳动经济学和其他金融以外的经济专题
--

---
PDF下载：
-->