Formalizing Arrow’s theorem
Formalizing Arrow’s theorem
复制标题
形式化阿罗定理
DOI：
10.1007/s12046-009-0005-1
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Wenzel
中科院分区：
文献类型：
--
作者：
M. Wenzel
我在这里介绍了一个小项目，在这个项目中，我使用Mizar系统在计算机中编码了阿罗定理的证明-可能是社会选择理论经济学领域最著名的结果。讨论了这一具体项目的细节，以及一般的形式化过程(在计算机中对校样进行编码)。
A small project in which I encoded a proof of Arrow’s theorem—probably the most famous results in the economics field of social choice theory—in the computer using the Mizar system is presented here. The details of this specific project, as well as the process of formalization (encoding proofs in the computer) in general are discussed.