Analysing Vote Counting Algorithms Via Logic
And its Application to the CADE Election System

Bernhard Beckert, Rajeev Gore, and Carsten Schürmann


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 our
method and system are applied to analyse the vote counting algorithm
used to elect CADE Trustees, we find that it strictly differs from the
standard definition of Single Transferable Vote (STV). We therefore
argue that it is a misnomer to say that the CADE algorithm implements
STV.