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.
This research project is one of a number of projects at this institution. It is in competition for funding with one or more of these projects. Usually the project which receives the best applicant will be awarded the funding. The funding is available to citizens of a number of European countries (including the UK). In most cases this will include all EU nationals. However full funding may not be available to all applicants and you should read the full department and project details for further information.
Supervisor's Webpage http://www.cs.man.ac.uk/~korovink/
How good is research at The University of Manchester in Computer Science and Informatics?
FTE Category A staff submitted: 44.86
Research output data provided by the Research Excellence Framework (REF)
Click here to see the results for all UK universities