Komplexpraktikum/Project "Reasoning in Description Logic" in SS 2003


Initial meeting
takes place on April 10 at 11:10 (3. DS) in Room 450. Attending the initial meeting is mandatory for participation in the praktikum/project.
People who want to participate in the praktikum/project, but have serious reasons to not attend the initial meeting, please sent an email until April 8.

Position in curriculum
- Diplomstudiengang Informatik (Diplom- und Bakkalaureatsabschluß), ab 5. Semester ;Wahlpflichtveranstaltung (-/-/4)
- Course of studies Computation Logic; project (12 credits)

Prerequisites
for computer scientists: Pflichtvorlesung "Grundlagen der Theoretischen Informatik"

Organisation
- An initial meeting is held at the beginning of the semester (see above). In this meeting, a brief presentation of the available topics will be given (see below). Students then have the opportunity to choose a topic to work on.
- Each student is assigned a tutor, depending on the topic chosen. During the semester, there will be regular meetings of the student and his tutor.
- The results of the praktikum/project will be presented at the end of the semester in a talk given by the student. Time and date are yet to be fixed.

Language
The language of the initial meeting will be English if attended by CL students, and German otherwise. Concerning the final presentations, students may choose to present their work in German or in English.

Participants Duties
The participants are expected to read the relevant literature, and to discuss it with their tutor in order to become acquainted with the topic chosen. The required implementation work should be carried out in a structured way, and has to be documented appropriately. If a topic is shared by two or more participants, acquiring team-working skills is another goal of the project. The results of the project have to be described in a essay (~15 pages) and presented in a 30 minutes talk at the end of the semester.

Topics
Some of the topics can be worked on by more than one student

(1) The Description Logic EL and recursively defined concepts.
EL is a Description Logic of rather limited expressive power, which nevertheless has interesting applications in medicine. Recently, we have shown that extending EL by recursively defined concepts leaves the relevant inference problems (like subsumption and instance) polynomial. The main tool to show this is to translate EL-terminologies into graphs, and show that subsumption/instance corresponds to the existence of certain simulation relations on graphs. The task is here to implement and optimize the (known) polynomial-time algorithms for computing simulation relations, and to test them on example knowledge bases.
Literature:
  • Franz Baader. Terminological Cycles in a Description Logic with Existential Restrictions. LTCS-Report 02-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2002.
  • Monika R. Henzinger, Thomas A. Henzinger and Peter W. Kopke. Computing Simulations on Finite and Infinite Graphs. 36th Annual Symposium on Foundations of Computer Science, IEEE Computer Society Press, Milwaukee, Wisconsin, 1995, 453--462.
  • William F. Dowling and Jean Gallier. Linear-time Algorithms for Testing the Satisfiability of Propositional Horn Formulae. Journal of Logic Programmming, 1(3):267--284, 1984.
Tutor: Franz Baader

(2) Implementation of optimized ALC-ALE Approximations
Approximation is a new reasoning service for description logics that has recently cought the attention of researchers. The purpose of this project is to enhance the existing LISP implementation of approximation for the description logics ALC and ALE by integrating two optimization techniques: (1) a special treatment of certain well-behaved (so called "nice") concepts and (2) implementation of the so-called "lazy unfolding" of acyclic TBoxes. Both implementations should then also be evaluated and compared.
Literature: Tutor: Anni-Yasmin Turhan.

(3) Translating description and modal logics.
State-of-the-art description logic (and modal logic) reasoning systems such as FaCT and RACER are based an tableaux-style decision procedures. This project is concerned with another approach to reasoning with such logics, namely the translation to weak second order logic in one successor (WS1S). Such translations, which are technically rather straightforward, are of interest due to the existence of highly optimized WS1S reasoners such as Mona. The goal of the project is to write a translator from description (or modal) logic formulas to WS1S formulas and to couple it with the Mona system. If time suffices, it would be interesting to investigate the run-time behaviour of the resulting system.
Literature: The Mona Manual (more to be supplied).
Tutor: Carsten Lutz,

(4) Design of an Ontology and description of the experiences made in the design.
The student may chose any non-trivial area he or she knows sufficiently well and describe the relevant concepts of this area using the ontology editors OilEd and Rice . The experiences made during this design phase should be described thoroughly, including a comparison of both editors.
Literature: S. Bechhofer, I. Horrocks, C. Goble, and R. Stevens. OilEd: a reason-able ontology editor for the semantic web. In Proc. of the Joint German Austrian Conference on AI, number 2174 in Lecture Notes In Artificial Intelligence, pages 396-408. Springer-Verlag, 2001.
Tutor: Ulrike Sattler,

(5) Concept generator for description logics.
to evaluate the quality of imlemented DL reasoning systems, it is very useful to generate a large amount of formulas with certain characteristics. The goal of this project is to implement a generator for description logic concepts (i.e., formulas) that takes several parameters, such as nesting depth and number of atomic concepts, and randomly generates a set of concepts in accordance with the input parameters.
Literature:
  • Ian P. Gent and Toby Walsh. Beyond NP: The QSAT Phase Transition. Proceedings of AAAI-99, 1999.
  • I. Horrocks, P. F. Patel-Schneider, and R. Sebastiani. An analysis of empirical testing for modal decision procedures. Logic Journal of the IGPL, 8(3):293-323, 2000.
Tutor: Jan Hladik

(6) Implementation of a matching algorithm for the Description Logic ALN.
A matching problem comprises a concept description and a so-called concept pattern, i.e., a concept description with variables. Matching a concept pattern against a concept description means finding a substitution of the occurring variables by concept descriptions such that the original concept description is subsumed by the instantiated concept pattern.
Since matching in the Description Logic ALN is theoretically well-examined this topic focusses on the implementation of the relevant algorithm in LISP and on the evaluation w.r.t. run-time behaviour.
Literature:
  • F. Baader, R. Küsters, A. Borgida, and D. McGuinness. Matching in Description Logics. Journal of Logic and Computation, 9(3):411-447, 1999.
  • S. Brandt. Matching under Side Conditions in Description Logics. Diploma thesis, RWTH Aachen, Germany, 2000.
  • Guy L., Jr. Steele. Common Lisp: The Language.
Tutor: Sebastian Brandt

Carsten Lutz