Rigorous treatment of Meek's method for single transferable vote with formal proofs of key properties
dc.contributor.advisor
Fleuriot, Jacques
dc.contributor.advisor
Papapanagiotou, Petros
dc.contributor.author
Palmer, Jake Evan
dc.contributor.sponsor
Engineering and Physical Sciences Research Council (EPSRC)
en
dc.date.accessioned
2023-08-14T15:19:51Z
dc.date.available
2023-08-14T15:19:51Z
dc.date.issued
2023-08-14
dc.description.abstract
This thesis presents a mechanised formalisation of key concepts and properties of Meek's method of Single Transferable Vote (STV). This method is currently in use in a number of local elections in New Zealand, the Royal Statistical Society, and even the Stack Exchange network. Using a formal approach, we show that the iterative solution to the surplus transfer round of Meek's method converges to a unique and valid solution, and connect a functional implementation of its key components to a more abstract and generalised proof.
Along the way, we consider and address issues present in existing pen-and-paper proofs, and discuss a general representation of strict ballots suitable for the proof patterns encountered in our formal development and for the implementation of Meek's method.
We believe that this work pushes the boundaries of interactive theorem proving for the formal verification of voting algorithms, and offers multiple promising avenues for further work on formally verifying the correctness and termination of STV methods in Isabelle/HOL.
en
dc.identifier.uri
https://hdl.handle.net/1842/40863
dc.identifier.uri
http://dx.doi.org/10.7488/era/3616
dc.language.iso
en
en
dc.publisher
The University of Edinburgh
en
dc.relation.hasversion
Schmoetten, R., Palmer, J. E., and Fleuriot, J. D. (2022). Towards formalising Schutz’ axioms for Minkowski spacetime in Isabelle/HOL. Journal of Automated Reasoning, 66(4):953–988.
en
dc.subject
Brian Lawrence Meek
en
dc.subject
Single Transferable Vote (STV)
en
dc.title
Rigorous treatment of Meek's method for single transferable vote with formal proofs of key properties
en
dc.title.alternative
A rigorous treatment of Meek's method for single transferable vote with formal proofs of key properties
en
dc.type
Thesis or Dissertation
en
dc.type.qualificationlevel
Doctoral
en
dc.type.qualificationname
PhD Doctor of Philosophy
en
Files
Original bundle
1 - 1 of 1
- Name:
- PalmerJE_2023.pdf
- Size:
- 1.04 MB
- Format:
- Adobe Portable Document Format
- Description:
This item appears in the following Collection(s)