Visualising Proof Search

Research areas

Temporary Supervisor

Professor John Slaney

Description

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

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.

Requirements

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:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing