KIT | KIT-Bibliothek | Impressum | Datenschutz

Verified Construction of Fair Voting Rules

Diekhoff, Karsten 1; Kirsten, Michael ORCID iD icon 1; Krämer, Jonas 1
1 Karlsruher Institut für Technologie (KIT)


Voting rules aggregate multiple individual preferences in order to make collective decisions. Commonly, these mechanisms are expected to respect a multitude of different fairness and reliability properties, e.g., to ensure that each voter's ballot accounts for the same proportion of the elected alternatives, or that a voter cannot change the election outcome in her favor by insincerely filling out her ballot. However, no voting rule is fair in all respects, and trade-off attempts between such properties often bring out inconsistencies, which makes the construction of arguably practical and fair voting rules non-trivial and error-prone.
In this paper, we present a formal and systematic approach for the flexible and verified construction of voting rules from composable core modules to respect such properties by construction. Formal composition rules guarantee resulting properties from properties of the individual components, which are of generic nature to be reused for various voting rules. We provide a prototypical logic-based implementation with proofs for a selected set of structures and composition rules within the theorem prover Isabelle/HOL. ... mehr

Postprint §
DOI: 10.5445/IR/1000120007
Veröffentlicht am 23.04.2021
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsdatum 22.04.2020
Sprache Englisch
Identifikator ISBN: 978-3-030-45259-9
ISSN: 0302-9743
KITopen-ID: 1000120007
Erschienen in Logic-Based Program Synthesis and Transformation : 29th International Symposium, LOPSTR 2019, Porto, Portugal, October 8–10, 2019, Revised Selected Papers. Ed.: M. Gabbrielli
Auflage 1st ed.
Verlag Springer International Publishing
Seiten 90–104
Serie Theoretical Computer Science and General Issues ; 12042
Schlagwörter Social choice, Higher-order logic, Modular verification
Nachgewiesen in Scopus
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page