Verifying randomised social choice

DOI10.1007/978-3-030-29007-8_14MaRDI QIDQ2180231zbMATH OpenOpenAlexFDO

Authors Manuel Eberl

Publication date 13 May 2020

Full work available at URL https://doi.org/10.1007/978-3-030-29007-8_14

Mathematics Subject Classification ID

Social choice (91B14) Formalization of mathematics in connection with theorem provers (68V20)

Recommendations

• Social choice theory in HOL. Arrow and Gibbard-Satterthwaite
• Automated reasoning in social choice theory: some remarks
• Formalizing Arrow's theorem
• Probabilistic guarded commands mechanized in HOL
• Verified analysis of random binary tree structures

Cited in

(3)

• Costly verification in collective decisions
• Voting theory in the Lean theorem prover
• Isabelle formalisation of original representation theorems

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• HOL

This page was built for publication: Verifying randomised social choice

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2180231)