A Calculus for Computing Structured Justifications for Election Outcomes

In the context of social choice theory, we develop a tableaubased calculus for reasoning about voting rules. This calculus can be used to obtain structured explanations for why a given set of axioms justifies a given election outcome for a given profile of voter preferences. We then show how to operationalise this calculus, using a combination of SAT solving and Answer Set Programming, to arrive at a flexible framework for presenting human-readable justifications to users.