Efficient automated theorem proving for first-order logic
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.
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. Applications for this project are welcome from suitably qualified candidates worldwide. Funding may only be available to a limited set of nationalities 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