Student research opportunities
Visualising Proof Search
Project Code: CECS_80
This project is available at the following levels:
Honours
Please note that this project is only for undergraduate students.
Keywords:
automated reasoning, information visualisation
Supervisor:
Dr John SlaneyOutline:
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. 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 use a generic information visualisation tool developed recently in NICTA's Canberra Lab, applying it to runtime data extracted from automated reasoning software to reveal interesting features of the proof search process. One outcome will be better insight into the process of reasoning. Another will be that we serve as a case study for improving the visualilsation tool.
Requirements/Prerequisites
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.
