Voting by Eliminating Quantifiers
Linköping University, Department of Computer and Information Science, KPLAB - Knowledge Processing Lab
Linköping University, The Institute of Technology
Article in journal (Refereed)
Studia Logica: An International Journal for Symbolic Logic(ISSN 0039-3215)(EISSN 1572-8730)
Engineering and Technology
Mathematical theory of voting and social choice has attracted much attention. In the general setting one can view social choice as a method of aggregating individual, often conflicting preferences and making a choice that is the best compromise. How preferences are expressed and what is the “best compromise” varies and heavily depends on a particular situation. The method we propose in this paper depends on expressing individual preferences of voters and specifying properties of the resulting ranking by means of first-order formulas. Then, as a technical tool, we use methods of second-order quantifier elimination to analyze and compute results of voting. We show how to specify voting, how to compute resulting rankings and how to verify voting protocols.