Dr K Korovin
Applications accepted all year round
Competition Funded PhD Project (European/UK Students Only)
About the Project
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.
Funding Notes
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.
References
Supervisor's Webpage http://www.cs.man.ac.uk/~korovink/
Continue with Facebook
