Decision Sciences & Systems
Technical University of Munich

Manuel Eberl (TUM): A Formal Proof of the Incompatibility of SD-Efficiency and SD-Strategy-Proofness

Wednesday, 07 September 2016 14:00
DSS Seminarraum (01.10.033)

In the design of voting rules, there are three intuitively desirable properties that one might reasonably expect such a rule to fulfil:

  • A voting rule should treat every voter and any alternative on the ballot equally.
  • The result should satisfy the voters as far as possible; i. e. there should be no other result that is obviously better for everyone.
  • No voter should be able to obtain an advantage by lying about her preferences.

These intuitively desirable properties have formal counterparts by the name of Anonymity and Neutrality, Efficiency, and Strategy-Proofness, respectively. It is well-known that the last two are in some way in conflict to one another – fulfilling both of them is often not possible or imposes great restrictions.

This work focuses on the setting of randomised voting with weak preferences (i. e. voters may submit preferences with ties), particularly on previous work by Brandl et al., who used computerised search and SMT solvers to prove a conjecture by Aziz et al. that no anonymous and neutral randomised voting rule (known as Social Decision Scheme) can fulfil the notions of both SD-Efficiency and SD-Strategy-Proofness. My work consists of a fully mechanised formal proof of this result using the interactive theorem prover Isabelle and, based upon this, a human-readable pen-and-paper proof. 


All Dates

  • Wednesday, 07 September 2016 14:00

Powered by iCagenda

Decision Sciences & Systems (DSS), Department of Informatics (I18), Technische Universität München, Boltzmannstr. 3, 85748 Garching, Germany
©2002-2018 DSS All Rights Reserved
Impressum, Privacy Policy, Copyright Information and Disclaimer