Implementation of a Tableau-based Decision Procedure 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.
The goal of the project is to implement the standard tableau-based decision procedure for checking concept satisfiability for the simple Description Logic ALC as well as well-known standard optimization techniques. The system will then be extended to take into account background knowledge (so-called TBoxes) during proof search too. Optional is the integration of additional language features (leading to more expressive DLs) .
The implementation should be done in Java. The system should be configurable in the sense that is easily possible to switch on / off the available optimizations.

The goal of the project is (a) to learn about DLs and (for simple DLs) about some classical proof procedures, (b) to learn how to implement such a (non-deterministic) procedure and (c) to see how proof search can be optimized and integrate a few well-known optimizations. An evaluation of the implemented procedure (and the effect of optimizations) could complete the project nicely.