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.

@InProceedings{BeckertGoreSchuermann2013,
author = {Bernhard Beckert and Rajeev Gor\'e and
Carsten Sch\"urmann},
title = {Analysing Vote Counting Algorithms Via Logic -
And its Application to the {CADE} Election System},
booktitle = {24th International Conference on Automated
Deduction (CADE-24)},
series = {LNCS},
volume = {7898},
editor = {Maria Paola Bonacina},
publisher = {Springer},
pages = {135-144},
doi = {10.1007/978-3-642-38574-2_9},
year = {2013},
month = jun,
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.},
place = {Lake Placid, NY, USA},
date = {June 9-14}
}