Analysing vote counting algorithms via logic: And its application to the CADE election scheme

Bernhard Beckert; Rajeev Goré; Carsten Schürmann

doi:10.1007/978-3-642-38574-2_9

Analysing vote counting algorithms via logic: And its application to the CADE election scheme

Bernhard Beckert
, Rajeev Goré
, Carsten Schürmann

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

6 Citations (Scopus)

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.

Original language	English
Title of host publication	CADE 2013 - 24th International Conference on Automated Deduction, Proceedings
Pages	135-144
Number of pages	10
DOIs	https://doi.org/10.1007/978-3-642-38574-2_9
Publication status	Published - 2013
Event	24th International Conference on Automated Deduction, CADE 2013 - Lake Placid, NY, United States Duration: 9 Jun 2013 → 14 Jun 2013

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	7898 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	24th International Conference on Automated Deduction, CADE 2013
Country/Territory	United States
City	Lake Placid, NY
Period	9/06/13 → 14/06/13

Access to Document

10.1007/978-3-642-38574-2_9

Cite this

Beckert, B., Goré, R., & Schürmann, C. (2013). Analysing vote counting algorithms via logic: And its application to the CADE election scheme. In CADE 2013 - 24th International Conference on Automated Deduction, Proceedings (pp. 135-144). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7898 LNAI). https://doi.org/10.1007/978-3-642-38574-2_9

Beckert, Bernhard ; Goré, Rajeev ; Schürmann, Carsten. / Analysing vote counting algorithms via logic : And its application to the CADE election scheme. CADE 2013 - 24th International Conference on Automated Deduction, Proceedings. 2013. pp. 135-144 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7b719b4576c742a09e3ef8a989a15b48,

title = "Analysing vote counting algorithms via logic: And its application to the CADE election scheme",

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.",

author = "Bernhard Beckert and Rajeev Gor{\'e} and Carsten Sch{\"u}rmann",

year = "2013",

doi = "10.1007/978-3-642-38574-2\_9",

language = "English",

isbn = "9783642385735",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "135--144",

booktitle = "CADE 2013 - 24th International Conference on Automated Deduction, Proceedings",

note = "24th International Conference on Automated Deduction, CADE 2013 ; Conference date: 09-06-2013 Through 14-06-2013",

}

Beckert, B, Goré, R & Schürmann, C 2013, Analysing vote counting algorithms via logic: And its application to the CADE election scheme. in CADE 2013 - 24th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7898 LNAI, pp. 135-144, 24th International Conference on Automated Deduction, CADE 2013, Lake Placid, NY, United States, 9/06/13. https://doi.org/10.1007/978-3-642-38574-2_9

Analysing vote counting algorithms via logic: And its application to the CADE election scheme. / Beckert, Bernhard; Goré, Rajeev; Schürmann, Carsten.
CADE 2013 - 24th International Conference on Automated Deduction, Proceedings. 2013. p. 135-144 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7898 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

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 - https://www.scopus.com/pages/publications/84879962688

U2 - 10.1007/978-3-642-38574-2_9

DO - 10.1007/978-3-642-38574-2_9

M3 - Conference Paper

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 -

Beckert B, Goré R, Schürmann C. Analysing vote counting algorithms via logic: And its application to the CADE election scheme. In CADE 2013 - 24th International Conference on Automated Deduction, Proceedings. 2013. p. 135-144. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-38574-2_9

Analysing vote counting algorithms via logic: And its application to the CADE election scheme

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this