Skip navigation
The Australian National University

Student research opportunities

Best-first proof search for non-classical logics

Project Code: CECS_959

This project is available at the following levels:
PhD
Please note that this project is only for higher degree (postgraduate) applicants.

Keywords:

logic automated reasoning theorem proving

Supervisor:

Professor John Slaney

Outline:

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.

Goals of this project

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.

Requirements/Prerequisites

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


Contact:



Updated:  10 August 2015 / Responsible Officer:  JavaScript must be enabled to display this email address. / Page Contact:  JavaScript must be enabled to display this email address. / Powered by: Snorkel 1.4