Formalizing Arrow's theorem
From MaRDI portal
Publication:1040010
DOI10.1007/s12046-009-0005-1zbMath1176.91039OpenAlexW2143444807WikidataQ56168713 ScholiaQ56168713MaRDI QIDQ1040010
Publication date: 23 November 2009
Published in: Sādhanā (Search for Journal in Brave)
Full work available at URL: https://www.ias.ac.in/describe/article/sadh/034/01/0193-0220
social choice theoryGibbard-Satterthwaite theoremArrow's theoremformalization of mathematicsMizarproof errors
Mechanization of proofs and logical operations (03B35) Computational methods for problems pertaining to game theory, economics, and finance (91-08) Social choice (91B14)
Related Items
Lyndon words formalized in Isabelle/HOL ⋮ Formalization and Execution of Linear Algebra: From Theorems to Algorithms ⋮ Social choice theory in HOL. Arrow and Gibbard-Satterthwaite ⋮ Foreword ⋮ Polygonal numbers ⋮ Flexary operations ⋮ Euler's partition theorem ⋮ Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL ⋮ An introduction to mechanized reasoning ⋮ Using Theorema in the Formalization of Theoretical Economics ⋮ Routh’s, Menelaus’ and Generalized Ceva’s Theorems
Uses Software
Cites Work
- Repairing proofs of Arrow's general impossibility theorem and enlarging the scope of the theorem
- Arrow's theorem and the Gibbard-Satterthwaite theorem: A unified approach
- Three brief proofs of Arrow's impossibility theorem
- A compendium of continuous lattices in MIZAR
- Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
- Towards Self-verification of HOL Light
- Formal certification of a compiler back-end or
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
