@InProceedings{KirstenCailloux2018, author = {Michael Kirsten and Olivier Cailloux}, editor = {Sandra Bringay and Juliette Mattioli}, title = {Towards automatic argumentation about voting rules}, booktitle = {4{\`{e}}me conf{\'{e}}rence sur les Applications Pratiques de l'Intelligence Artificielle ({APIA} 2018)}, editor = {Sandra Bringay and Juliette Mattioli}, year = {2018}, abstract = {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. \newline 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.}, month = jul, url = {https://hal.archives-ouvertes.fr/hal-01830911}, venue = {Nancy, France}, eventdate = {2018-07-02/2018-07-06} }
Towards automatic argumentation about voting rules
Author(s): | Michael Kirsten and Olivier Cailloux |
---|---|
In: | 4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018) |
Year: | 2018 |
URL: | https://hal.archives-ouvertes.fr/hal-01830911 |
Abstract
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.