Efficient automated theorem proving for first-order logic

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 theorem proving has applications ranging from proving theorems in mathematics to verifying correctness of hardware and software. Automated theorem proving is rooted in mathematical logic and combines theoretical methods such as completeness theorems for logical calculi and decision procedures together with implementation techniques for efficient inferences and simplifications. Although theorem proving had a considerable success over recent years many problems coming from applications are still out of reach for current theorem proving methods.This PhD will be focused on developing novel theoretical and practical methods for making automated theorem proving scale to problems that can not be solved by the current state-of-the-art automated methods. The candidate is expected to have a strong background in logic and/or formal methods, good implementation skills are desirable.

▲ Up to the top