Automated Reasoning in Higher-Order Logic

Primary supervisor

Additional supervisors

  • Giles Reger

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.

James Elson studentship advertisement image

Project description

Automated Reasoning (AR) is one of the oldest sub-fields of Artificial Intelligence (AI) and is the study of mechanical reasoning about statements, typically formalised in logic. Beyond applications to pure reasoning problems, AR has applications in many areas of AI and beyond, including planning, question answering, program analysis, verification, security, and semantic web.

The prominent sub-field of automated deduction focuses on establishing the consistency, or otherwise, of a statement formalised in logic. Manchester is world-leading in the area of automated deduction for first-order logic and its Vampire theorem prover consistently wins the World Cup in first-order theorem proving and other international competitions. However, many sub-fields of AI research focus on, or could be enhanced by, reasoning in higher-order logic. Reasoning in higher-order logic has historically been the domain of interactive theorem provers, requiring human interaction, and although there has been some recent progress in automated techniques there remain many unsolved problems.

This project focuses on exploring the adaptation and extension of first-order techniques to the higher-order setting. This will involve the development of new pre-processing and inference techniques to be implemented within the Vampire theorem prover. The underlying hypothesis of this project, supported by our previous work, is that significant progress can be made by utilising existing technology and extending this using experiment-driven heuristics and translations. The aim will be to quickly transform Vampire into a world-leading reasoning system for higher-order logic.

This project would be ideally suited for someone with an interest in formal logic and reasoning, and its application within Artificial Intelligence. Prior knowledge of higher-order logic is not necessary but the ideal candidate would be familiar with first-order logic and associated reasoning techniques.

This project is eligible for The James Elson Studentship Award in Artificial Intelligence. The James Elson Studentship will provide an outstanding candidate with fees and an enhanced stipend to carry out a 3-year PhD research project relating to artificial intelligence. The School of Computer Science offers this prestigious PhD studentship for September 2017 entry, for students from the UK and EU who are eligible to pay 'Home' fees.

The deadline for applications for this studentship is Friday 17th March.

▲ Up to the top