KIT | KIT-Bibliothek | Impressum | Datenschutz

Towards automatic argumentation about voting rules

Kirsten, Michael ORCID iD icon; Cailloux, Olivier


Voting rules aggregate a group's preferences to make decisions. As multiple reasonable voting rules exist,
the axiomatic approach has been proposed to exhibit both their merits and paradoxical behaviors. It is however a difficult task to characterize a voting rule by such axioms, and even when a proof exists, it may be difficult to understand why a specific rule fails to satisfy a given axiom. In this article, we present an automatic method which
determines whether a given rule satisfies a set of axioms. It produces evidence which can be used by non-expert users to comprehend why a rule violates some axiom and may serve to argue in favor of rules which satisfy it. Our method is based on the software analysis technique “bounded model checking”, which enables bounded verification of software programs. The method can be applied to arbitrary voting rules; we demonstrate it on the case of the Borda axiomatization and compare the Borda rule to both the Black and the Copeland voting rules.

Verlagsausgabe §
DOI: 10.5445/IR/1000092711
Veröffentlicht am 28.03.2019
Cover der Publikation
Zugehörige Institution(en) am KIT Institut für Theoretische Informatik (ITI)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Proceedingsbeitrag
Publikationsjahr 2018
Sprache Englisch
Identifikator urn:nbn:de:swb:90-927118
KITopen-ID: 1000092711
Erschienen in 4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle, APIA 2018, Nancy, France, July 2-3, 2018., Ed.: S. Bringay, J. Mattioli
Schlagwörter social choice theory, bounded model checking, argumentation theory, automated reasoning
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page