Breaking Symmetries in Automated Reasoning

Primary supervisor

Additional information

Contact admissions office

Other projects with the same supervisor


  • Competition Funded Project (European/UK Students Only)
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.

Project description

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.

Person specification

For information


Applicants will be required to evidence the following skills and qualifications.

  • You must be capable of performing at a very high level.
  • You must have a self-driven interest in uncovering and solving unknown problems and be able to work hard and creatively without constant supervision.


Applicants will be required to evidence the following skills and qualifications.

  • You will possess determination (which is often more important than qualifications) although you'll need a good amount of both.
  • You will have good time management.


Applicants will be required to address the following.

  • Discuss your final year Undergraduate project work - and if appropriate your MSc project work.
  • How well does your previous study prepare you for undertaking Postgraduate Research?
  • Comment on your transcript/predicted degree marks, outlining both strong and weak points.
  • Why do you believe you are suitable for doing Postgraduate Research?
▲ Up to the top