Social Choice Theory in HOL

被引：3
|
作者：
Nipkow, Tobias [1 ]
机构：
[1] Tech Univ Munich, Inst Informat, Munich, Germany
来源：
JOURNAL OF AUTOMATED REASONING | 2009年 / 43卷 / 03期
关键词：
Social choice theory; Arrow's theorem; Gibbard-Satterthwaite theorem; Higher-order logic; Theorem proving; ARROWS THEOREM; WELFARE;
D O I：
10.1007/s10817-009-9147-4
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
This article presents formalizations in higher-order logic of two proofs of Arrow's impossibility theorem due to Geanakoplos. The Gibbard-Satterthwaite theorem is derived as a corollary. Lacunae found in the literature are discussed.
引用
收藏
页码：289 / 304
页数：16
相关论文
共 50 条
12345