Email Gateway (Nov 18 2022 at 10:08): Email Gateway (Nov 18 2022 at 10:08):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear all,
I'm happy to announce a new AFP entry:
Théo Delemazure, Tom Demeulemeester, Manuel Eberl, Jonas Israel, and Patrick Lederer:
The Incompatibility of Strategy-Proofness and Representation in Party-Approval
Multi-Winner Elections
Abstract:
In party-approval multi-winner elections, the goal is to allocate the seats of a
fixed-size committee to parties based on approval ballots of the voters over the parties.
In particular, each can approve multiple parties and each party can be assigned multiple
seats.
Three central requirements in this settings are:
Anonymity:
The result is invariant under renaming the voters.
Representation:
Every sufficiently large group of voters with similar preferences is represented by
some committee members.
Strategy-proofness:
No voter can benefit by misreporting her true preferences.
We show that these three basic axioms are incompatible for party-approval multi-winner
voting rules, thus proving a far-reaching impossibility theorem.
The proof of this result is obtained by formulating the problem in propositional logic and
then letting a SAT solver show that the formula is unsatisfiable. The DRUP proof output by
the SAT solver is then converted into Lammich's GRAT format and imported into Isabelle/HOL
with some custom-written ML code.
This transformation is proof-producing, so the final Isabelle/HOL theorem does not rely on
any oracles or other trusted external trusted components.
https://www.isa-afp.org/entries/PAPP_Impossibility.html
Enjoy,
Andreas
Last updated: Apr 24 2024 at 01:07 UTC