Voting Theory in the Lean Theorem Prover
Voting Theory in the Lean Theorem Prover
复制标题
精益定理证明中的投票理论
DOI：
10.1007/978-3-030-88708-7_9
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
E. Pacuit
中科院分区：
文献类型：
--
作者：
W. Holliday;Chase Norman;E. Pacuit
逻辑和社会选择理论之间卓有成效的互动有着悠久的传统。近年来，这种互动的大部分都集中在计算机辅助方法上，如SAT求解和交互式定理证明。在本文中，我们报告了在Lean定理证明器中形式化投票理论的框架的发展，并应用该框架来验证最近研究的一种投票方法的性质。虽然以前的交互定理证明在社会选择中的应用(使用Isabelle/HOL和Mizar)集中在不可能性定理的验证上，但我们的目标是涵盖从不可能性定理到特定投票方法的性质(例如Condorcet一致性、克隆的独立性等)的各种结果。为了形式化关于增加或删除候选人和投票人的投票理论公理，我们工作在一个可变的选举环境中，其形式化利用了Lean中的依赖类型。
There is a long tradition of fruitful interaction between logic and social choice theory. In recent years, much of this interaction has focused on computer-aided methods such as SAT solving and interactive theorem proving. In this paper, we report on the development of a framework for formalizing voting theory in the Lean theorem prover, which we have applied to verify properties of a recently studied voting method. While previous applications of interactive theorem proving to social choice (using Isabelle/HOL and Mizar) have focused on the verification of impossibility theorems, we aim to cover a variety of results ranging from impossibility theorems to the verification of properties of specific voting methods (e.g., Condorcet consistency, independence of clones, etc.). In order to formalize voting theoretic axioms concerning adding or removing candidates and voters, we work in a variable-election setting whose formalization makes use of dependent types in Lean.
通过SMT求解证明效率和策略证明的不相容性
DOI：
10.1145/3125642
发表时间：
2018
期刊：
Journal of the ACM (JACM)
影响因子：
--
作者：
Florian Brandl;Felix Brandt;Manuel Eberl;Christian Geist
通讯作者：
Christian Geist