CADE 2013 - LNAI 7898

Analysing Vote Counting Algorithms via Logic

And Its Application to the CADE Election Scheme

Bernhard Beckert¹, Rajeev Goré², and Carsten Schürmann³

¹Karlsruhe Institute of Technology, Germany
beckert@kit.edu

²The Australian National University, Australia
Rajeev.Gore@anu.edu.au

³IT University of Copenhagen, Denmark
carsten@itu.dk

Abstract. We present a method for using first-order logic to specify the semantics of preferences as used in common vote counting algorithms. We also present a corresponding system that uses Celf linear-logic programs to describe voting algorithms and which generates explicit examples when the algorithm departs from its specification. When we applied our method and system to analyse the vote counting algorithm used for electing the CADE Board of Trustees, we found that it strictly differs from the standard definition of Single Transferable Vote (STV). We therefore argue that “STV” is a misnomer for the CADE algorithm.

LNAI 7898, p. 135 ff.

Full article in PDF | BibTeX