Towards automatic argumentation about voting rules

Reviewed Paper In Proceedings

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.

BibTeX

@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}
}