Show simple item record

Towards automatic argumentation about voting rules

hal.structure.identifier
dc.contributor.authorKirsten, Michael
hal.structure.identifierLaboratoire d'analyse et modélisation de systèmes pour l'aide à la décision [LAMSADE]
dc.contributor.authorCailloux, Olivier
HAL ID: 16494
ORCID: 0000-0003-3244-1081
dc.date.accessioned2020-11-04T14:22:54Z
dc.date.available2020-11-04T14:22:54Z
dc.date.issued2018
dc.identifier.urihttps://basepub.dauphine.fr/handle/123456789/21187
dc.language.isoenen
dc.subjectSocial choice theoryen
dc.subjectbounded model checkingen
dc.subjectargumentation theoryen
dc.subjectautomated reasoningen
dc.subject.ddc003en
dc.titleTowards automatic argumentation about voting rulesen
dc.typeCommunication / Conférence
dc.description.abstractenVoting rules aggregate the preferences of a group to make decisions. As multiple reasonable voting rules exist, the ax-iomatic approach has been proposed to exhibit both their merits and paradoxical behaviors. It consists in characterizing a voting rule by a set of understandable properties called axioms. 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 voting rule fails to satisfy a given axiom, especially for untrained users. In this article, we present an automatic method which determines whether a given rule satisfies a set of axioms. When the rule does not satisfy an axiom, the automatic prover generates comprehensible evidence of the violation in the form of a counterexample. It can be used by non-expert users to comprehend the violation and may serve to argue in favor of other rules which satisfy the axiom. Our method is based on the software analysis technique bounded model checking, which enables bounded verification for properties of software programs. It translates the program together with user-annotations into a reachability problem for those profiles and outcomes which adhere to our specification. 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.en
dc.identifier.urlsitehttps://hal.archives-ouvertes.fr/hal-01830911en
dc.subject.ddclabelRecherche opérationnelleen
dc.relation.conftitle4ème conférence sur les Applications Pratiques de l'Intelligence Artificielle (APIA 2018)en
dc.relation.confdate2018-07
dc.relation.confcityNancyen
dc.relation.confcountryFranceen
dc.relation.forthcomingnonen
dc.description.ssrncandidatenonen
dc.description.halcandidatenonen
dc.description.readershiprechercheen
dc.description.audienceInternationalen
dc.relation.Isversionofjnlpeerreviewednonen
dc.relation.Isversionofjnlpeerreviewednonen
dc.date.updated2020-11-04T14:17:36Z
hal.author.functionaut
hal.author.functionaut


Files in this item

FilesSizeFormatView

There are no files associated with this item.

This item appears in the following Collection(s)

Show simple item record