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

Verified Construction of Multi-Round and Scoring-based Voting Rules Using Isabelle/HOL

Forschungsthema:Computational Social Choice
Typ: BA
Datum: 2025-01-15
Betreuer: Michael Kirsten
Aushang:

Abstract

Voting rules play a crucial role in aggregating individual preferences into collective decisions, with applications ranging from political elections to group decision-making.

In this thesis, I extend a formal voting rule construction framework within the theorem prover Isabelle/HOL to both multi-round and scoring-based voting rules. While the framework allows the modular design of various voting rules, it faces limitations with multi-round (iterative or multi-stage winner determination) and scoring-based methods (where voters assign scores instead of rankings).

To address these gaps, I introduce the MAX-𝑛-Eliminator and the rank-loop composition for constructing new such voting methods. I implemented Bucklin voting, runoff voting, and STAR voting together with the Condorcet loser criterion and the resolvability criterion as social choice properties into the framework. Moreover, I conduct a case study on range voting for the resolvability criterion, and evaluate the effects of my extensions on existing compositions in the framework.

Literature