Social choice theory in HOL. Arrow and Gibbard-Satterthwaite

DOI10.1007/s10817-009-9147-4zbMath1185.68631OpenAlexW1840672264WikidataQ56659149 ScholiaQ56659149MaRDI QIDQ2655324

Tobias Nipkow

Publication date: 25 January 2010

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-009-9147-4

zbMATH Keywords

theorem provinghigher-order logicsocial choice theoryGibbard-Satterthwaite theoremArrow's theorem

Mathematics Subject Classification ID

Related Items (11)

Algorithmic Decision Theory Meets Logic ⋮ Voting theory in the Lean theorem prover ⋮ Representing voting rules in Łukasiewicz’s three-valued logic ⋮ First-order logic formalisation of impossibility theorems in preference aggregation ⋮ Arrow's decisive coalitions ⋮ Foreword ⋮ 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 ⋮ Arrow Gibbard Satterthwaite ⋮ Formalizing Arrow's theorem

Uses Software

• Isabelle/HOL
• Social Choice Theory
• Archive Formal Proofs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Formalizing Arrow's theorem
• Repairing proofs of Arrow's general impossibility theorem and enlarging the scope of the theorem
• Strategy-proofness and Arrow's conditions: existence and correspondence theorems for voting procedures and social welfare functions
• Arrow's theorem and the Gibbard-Satterthwaite theorem: A unified approach
• Isabelle/HOL. A proof assistant for higher-order logic
• Three brief proofs of Arrow's impossibility theorem
• Manipulation of Voting Schemes: A General Result

This page was built for publication: Social choice theory in HOL. Arrow and Gibbard-Satterthwaite