Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Arrow's Impossibility Theorem

Email Gateway (Aug 18 2022 at 12:29):

From: Tobias Nipkow <nipkow@in.tum.de>
A new entry has been added to the development version of the Archive of
Formal Proofs:

Arrow and Gibbard-Satterthwaite

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.

http://afp.sourceforge.net/devel-entries/ArrowImpossibilityGS.shtml

An accompanying paper: http://www.in.tum.de/~nipkow/pubs/arrow.html

Enjoy
Tobias

Last updated: Nov 21 2024 at 12:39 UTC