MSc Project I: A Java GUI for visualizing tableau computation graphs
The aim of this project is to implement a visualization tool that allows to display graphical representations of
tableau computations. Those computations are carried out by a system that decides the satisfiability
problem for a certain temporalized description logic. The algorithm in use has various optimization
options which basically prune a search tree according to heuristic rules. In order to observe the
effects of those heuristics, it is essential to be able to visualize the tree.
As input for the tool there will be given a file containing information about nodes and edges in
GML format (Graph Modelling
Language). Node descriptions comprise references to a collection
of GIF image files which are to be displayed in the tree.
There are two different kinds of edges -- ordinary edges of the tree and special edges that can
connect any leaf of the tree with any other node.
Subtasks to be performed include:
- parsing of the GML file (simple tree and additional special edges)
- displaying the tree and the referenced GIF image files at the nodes down to a given depth in a "nice" way
- displaying the two sorts of edges in different colour
- showing the number of remaining nodes in not fully expanded subtrees
- allow to expand subtrees specifically
- allow to shift nodes in order to get a better picture
The visualization tool will be used for:
- testing the tableau algorithm and its optimization options
- demonstrating rules and optimizations (which might prune the tree) for teaching purposes
- optimizing itself -- one might recognize typical structures and identify "hard" subformulas
-- information that can be used to investigate further optimization techniques
Java is suggested as programming language for the implementation, portability to Windows and Linux
resp. should be ensured. A suitable graphic library should be chosen. The student must have some
experience with (GUI)programming in Java and in using some graphic library.
Knowledge about logic and tableau algorithms is not required.