Mon, 2007-05-07 20:50 — pietro

==Background==
Tableau calculi are now routinely used to determine whether or not a particular statement A is a logical consequence of another collection of statements Gamma in some (non-classical) logic L. Such provers have applications in Hardware Verification, Artificial Intelligence and Hybrid Systems. Tableau calculi (and sequent calculi) can be efficiently automated for a broad range of logics.
Pietro Abate has built a generic theorem prover called the Tableau WorkBench [1]. This prover can be programmed with a new set of tableau rules to create a theorem prover for your favourite logic. Proofs in such calculi tend to be n-ary (cyclic) trees.
Visualizing large proof trees at the moment is an open area of research [2]. While the reasoning capabilities of interactive proof systems have increased markedly in recent years, the system interfaces have often not enjoyed the same attention as the proof engines themselves. In many cases, interfaces remain basic and under-designed.
The tableau workbench currently has only a basic user interface that makes it difficult to use for the naive user.
==Honours student research project==
Your task will be to join the research that we are doing on tableau-based theorem proving by adding a user interface to the TWB and modifying the TWB by adding a framework to extracting counter models from failed proofs.
===Counter model extraction:===
* An important aspect of tableau-based theorem proving since failure to find a proof can give useful insights to the user. The TWB currently has no explicit mechanism for the extraction of counter-models, although it does have a rudimentary trace facility from which users could extract counter-models by hand.
* You will need to become familiar with sequent and tableau proof calculi for various nonclassical logics, and become familiar with modal logic (local expertise abounds). You will need to become familiar with the TWB. This project is likely to be extensible to a Phd topic and our previous students have published their work in international conferences and journals.
===Visualizing large proof trees:===
* For starters you would be expected to create a widget to display proof trees, integrate it to the existing prover and in a usable GUI. You will need to be familiar with XML [3] and learn about XUL [4], JS, C++, Ocaml [5] and related technologies [6]. The main goal of this subproject is to offer a web based user interface to the TWB as well as a general toolkit to display proof trees based on a XML specification.
This is not just a programming task because GUIs for theorem provers are a emerging research are in their own right [2]. This work could easily lead to a new XML standard for displaying proof trees with applications in many other theorem provers apart from the TWB.
You will need a strong background computer science. A grounding in functional programming and logic would be useful but is not essential as there is plenty of local expertise in this area.
# [http://twb.rsise.anu.edu.au TWB Home Page ]
# [ http://www.etaps05.inf.ed.ac.uk/Workshops/workshop.html#uitp Workshop on User Interfaces for Theorem Provers ]
# [ http://www.w3.org/XML/ XML ]
# [ http://www.mozilla.org/projects/xul/ XUL ]
# [ http://www.ocaml.org/ OCAML ]
# [ http://books.mozdev.org/chapters/index.html OCaml Related Technologies ]