  We introduce a logic specifically designed to support reasoning about social
choice functions. The logic includes operators to capture strategic ability,
and operators to capture agent preferences. We establish a correspondence
between formulae in the logic and properties of social choice functions, and
show that the logic is expressively complete with respect to social choice
functions, i.e., that every social choice function can be characterised as a
formula of the logic. We prove that the logic is decidable, and give a complete
axiomatization. To demonstrate the value of the logic, we show in particular
how it can be applied to the problem of determining whether a social choice
function is strategy-proof.

Multiagent Systems