Spreading excellence and disseminating the cutting edge results of our research and development efforts is crucial to our institute. Check for our educational offers for Bachelor, Master and PhD studies at the University of Innsbruck!

Exploring Propositional Local-Search Procedures for Tableau-based Reasoning in the Description Logic ALC

Student name: 
Adrian Marte
PDF icon adrian-marte-bachelor-2008.pdf444.62 KB

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

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 developed an interesting algorithmic framework for Tableau-methods, which are the most wide-spread and successful class of methods for solving the satisfiability problem of concept descriptions (or modal formula respectively). The satisfiabilty problem in fact is one of the most fundamental forms of reasoning, a number of interesting reasoning problems can be expressed as satisfiability problems. A well known example is the test if a given statement is entailed by a set of statements. Hence, efficient algorithms solving the satisfiability problem can be used to solve any of these problems too.
The goal of the project is to explore the use of a specific class of propositional satisfiability tests in the context of our novel algorithmic framework. More specifically, the project is about taking a number of stochastic local search (SLS) methods and investigate their use in our setting.
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 about our algorithmic framework, (c) to learn about SLS methods for propositional logic, (d) to integrate them in our framework and (e) to investigate and evaluate their use in our setting.