Verifying Randomised Social Choice
by Manuel Eberl
In: Proceedings of FroCoS 2019
Best Paper by a Junior Researcher
DOI:
10.1007/978-3-030-29007-8_14Abstract:
This work describes the formalisation of a recent result from Randomised Social Choice Theory in Isabelle/HOL. The original result had been obtained through the use of linear programming, an unverified Java program, and SMT solvers; at the time that the formalisation effort began, no human-readable proof was available. Thus, the formalisation with Isabelle eventually served as both independent rigorous confirmation of the original result and led to human-readable proofs both in Isabelle and on paper.
This presentation focuses on the process of the formalisation itself, the domain-specific tooling that was developed for it in Isabelle, and how the structured human-readable proof was constructed from the SMT proof. It also briefly discusses how the formalisation uncovered a serious flaw in a second peer-reviewed publication.
Download preprint PDF (452 KiB)
BibTeX:
@inproceedings{eberl19rsc,
author="Eberl, Manuel",
title="Verifying Randomised Social Choice",
year="2019",
booktitle="Frontiers of Combining Systems"
}