[isabelle] Newer in the AFP: Social Choice (Part II)



Manuelâs second AFP contribution is now online. This is a direct application of his Randomised Social Choice development.

Larry Paulson



The Incompatibility of SD-Efficiency and SD-Strategy-Proofness
Manuel Eberl

This formalisation contains the proof that there is no anonymous and neutral Social Decision Scheme for at least four voters and alternatives that fulfils both SD-Efficiency and SD-Strategy- Proofness. The proof is a fully structured and quasi-human-redable one. It was derived from the (unstructured) SMT proof of the case for exactly four voters and alternatives by Brandl et al. Their proof relies on an unverified translation of the original problem to SMT, and the proof that lifts the argument for exactly four voters and alternatives to the general case is also not machine-checked. In this Isabelle proof, on the other hand, all of these steps are fully proven and machine-checked. This is particularly important seeing as a previously published informal proof of a weaker statement contained a mistake in precisely this lifting step.

http://www.isa-afp.org/entries/SDS_Impossibility.shtml





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