Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Distance Rationalization for Modular Construction of Verified Voting Rules

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2021-08-16
Betreuer: Michael Kirsten
Aushang:

Abstract

Voting rules are procedures that map the preferences of several voters to a collective decision. The process of distance rationalizing a voting rule means to interpret them as procedures that elect an uncontroversial winner if there is one, and otherwise elect the candidates that are as close to becoming an uncontroversial winner as possible. We can use distance rationalization as a modular construction scheme for voting rules: The choice of three components - a distance on votes, a norm and a consensus class - characterizes a voting rule. Moreover, some desirable fairness properties of voting rules can be inferred from properties of such components, each satisfied by several voting rule instances simultaneously.
In this thesis, we formalize distance rationalization as an extension of the verified construction framework within Isabelle/HOL. We add suitable lemmata and construction rules to the inference rules for the two properties of anonymity and monotonicity, and verify the anonymity proof within Isabelle/HOL. In our evaluation, we apply the formalized construction rules and the anonymity proof to the two voting rules by Kemeny and Borda, and thereby demonstrate the use of our framework extensions.

Literature