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