Implementation and visualization of the BDD-Tableau Calculus for the Description Logic ALC

Description Logics (DLs) are a family of class-based
knowledge representation formalisms characterised by the use of
various constructors to build complex classes from simpler ones, and
by an emphasis on the provision of sound, complete and (empirically)
tractable reasoning services. They have a range of applications, but
are most widely known as the basis for ontology languages such as
OWL.
A specifically simple Description Logic is the logic ALC. ALC can be seen as a syntactic variant of the (multi-)modal logic K.
Recently, we designed a specific decision procedure for ALC for a very fundamental reasoning service in DLs, namely checking the satisfiability of a given concept (or class) description.
The procedure combines Binary Decision Diagrams (BDDs) with DL Tableau and allows for integration of background knowledge (so-called TBoxes).
The goal of the project is to implement this specific decision procedure for checking concept satisfiability for the simple Description Logic ALC and to provide a simple graphical environment that allows to (a) visualize the progress of the reasoning system and (b) to interactively affect the progress of the procedure.
The implementation should be done in Java.

The handling and management of BDD (and computation of operations on them) is covered by existing Java packages. Further, there already exist Java packages for displaying and interacting with graph structures.

Therefore a main task in the project is to (a) get familiar with existing libraries and to define how to combine them suitably, (b) to add functionality on top that allows to represent and visualize proofs in the given decision procedure and (c) to develop simple means to control proof search (interactively and perhaps at a later stage automatically).