Distance Rationalization for Modular Construction of Verified Voting Rules
|Forschungsthema:||Computational Social Choice|
Voting rules are procedures that map the preferences of several voters to a
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
We can use distance rationalization as a modular construction scheme for voting
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
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.
- "Automated Verification for Functional and Relational Properties of Voting Rules" in Sixth International Workshop on Computational Social Choice (COMSOC 2016)
- "Verified Construction of Fair Voting Rules" in 29th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2019)