Skip navigation
The Australian National University

Student research opportunities

Visualising Proof Search

Project Code: CECS_80

This project is available at the following levels:
Honours, Summer Scholar, Masters


automated reasoning, information visualisation


Professor John Slaney


This is a project in information visualisation, using computer graphics in creative ways to advance scientific understanding of the process of logical reasoning.

Automated reasoning systems search for proofs by repeatedly making inferences from what they already know, thus collecting a pool of known consequences that can be used as input for more inferences. The resulting space of proof fragments is potentially infinite, though of course only an initial segment of it will actually be explored by the reasoning system. In order to understand this process better, we need to apply visualisation tools to produce animated pictures of what is going on. Little research has been done on this, so it is very much an open area.

Goals of this project

We shall develop new information visualisation tools and apply them to runtime data extracted from existing theorem provers to reveal interesting features of the proof search process. Tools could be built from scratch or could be based on similar ones developed recently in NICTA's Canberra Lab. One outcome will be better insight into the process of reasoning. Another will be an advance in information visualisation for complex software processes.


Imagination, creative thinking, willingness to give ideas a go. Some competence with scripting languages or Java programming skills would be useful. Deep knowledge of automated theorem proving is not required, though some familiarity could help. Many theorem provers are in C or C++, so those languages would be relevant.


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