[isabelle] New AFP entry: The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency



The Incompatibility of Fishburn-Strategyproofness and Pareto-Efficiency
Felix Brandt, Manuel Eberl, Christian Saile and Christian Stricker

This formalisation contains the proof that there is no anonymous Social Choice Function for at least three agents and alternatives that fulfils both Pareto-Efficiency and Fishburn-Strategyproofness. It was derived from a proof of Brandt et al., which relies on an unverified translation of a fixed finite instance of the original problem to SAT. This Isabelle proof contains a machine-checked version of both the statement for exactly three agents and alternatives and the lifting to the general case.

https://www.isa-afp.org/entries/Fishburn_Impossibility.html

Enjoy!

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.