Best-first proof search for non-classical logics

Research areas

Temporary Supervisor

Professor John Slaney


Most techniques for searching for proofs in non-classical propositional logics proceed either by traversing a tree in a depth-first way or else by translation to (undecidable) classical first order logic. In this project, we explore the middle way of representing the search space as a constraint graph of formulae or sequents and attempting to find the best points at which to expand it, rewriting items and propagating decisions through the graph as we go. This is a very general account of top-down proof search, which is normally obscured by the depth-first search algorithm enforced by standard approaches. The hope is that thinking in a more generic way will result in more efficient theorem provers for a range of logics including systems of practical significance such as temporal logics.


To devise and implement new algorithms for proof search in a range of propositional logics; To investigate and better understand proof search spaces and the elements of algorithms for exploring them; To produce new theorem proving programs that will extend the boundaries of practical provability.


Essential: knowledge of elementary logic. Essential: competence in programming and software experimentation Highly desirable: knowledge of some non-classical logics Highly desirable: knowledge of some automated reasoning methods, such as SAT solving

Updated:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing