TY - GEN
T1 - Analysing vote counting algorithms via logic
T2 - 24th International Conference on Automated Deduction, CADE 2013
AU - Beckert, Bernhard
AU - Goré, Rajeev
AU - Schürmann, Carsten
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84879962688&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-38574-2_9
DO - 10.1007/978-3-642-38574-2_9
M3 - Conference contribution
SN - 9783642385735
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 135
EP - 144
BT - CADE 2013 - 24th International Conference on Automated Deduction, Proceedings
Y2 - 9 June 2013 through 14 June 2013
ER -