Home  |  deutsch  |  Legals  |  Data Protection  |  Sitemap  |  KIT

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

Reviewed Paper In Proceedings

Author(s):Bernhard Beckert, Rajeev Goré, and Carsten Schürmann
In:24th International Conference on Automated Deduction (CADE-24)
Publisher:Springer
Series:LNCS
Volume:7898
Year:2013
Pages:135-144
DOI:10.1007/978-3-642-38574-2_9

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.

BibTeX

@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}
}