Voting by Eliminating Quantifiers

Mathematical theory of voting and social choice has attracted much at-
tention. 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.