The aim of this project is to implement the workflow described by Geist and Peters [1] for generating concise human-readable mathematical proofs for theorems via the use of SAT solvers. Initially the focus will be on theorems in the area of social choice, before potentially branching out into argumentation theory or matching theory. The project will involve research on automated theorem proving, SAT solvers, explainable AI (XAI).

Possible project outputs include: - Comparison of the performance of different SAT solvers - Website allowing users to explore different proofs of some of the main results in social choice (e.g., Arrow’s Impossibility Theorem). - Discovery of new theorems in argumentation theory.

[1] C. Geist and D. Peters, Computer-Aided Methods for Social Choice Theory, in Trends in Computational Social Choice, 2017