Breaking Symmetries in Automated Reasoning

Automated reasoning has a wide range of applications including verification of software and hardware, reasoning with ontologies and proving mathematical theorems. Many reasoning problems have intrinsic symmetries. Exploiting such symmetries can dramatically speed-up reasoning methods and allow us to solve problems which were not possible to solve otherwise. There are two major issues here: 1) discovering symmetries in problems and 2) eliminating symmetric search space to speed-up reasoning.
Although some research has been done on symmetry breaking for propositional reasoning the case of more expressive logics such as first-order logic or logics enriched with theories (aka SMT) is mostly an unexplored area. This project is focused on exploring novel methods for discovery symmetries in first-order and SMT problems and adapt reasoning systems to exploit such symmetries.
The developed algorithms will be integrated into state-of-the-art reasoning tools and extensively evaluated over a wide range of problems taken from TPTP and SMT benchmarks. There will be also exciting opportunities to apply developed methods to real-life verification problems coming from collaboration with Intel.

Requirements: strong interest in logic and willingness implementing and experimenting with new ideas.