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