Komplexpraktikum/Project "Automated Reasoning in Logical Formalisms" in WS 2003/04
 Initial
meeting
 takes place on October 17 at
11:10 (3. DS) in Room 454. 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 send 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); module TCSL
 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 is English. 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 teamworking
skills is another goal of the project. The results of the project have
to be described in a project paper (~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. Further
topics will be added in due course.
 (1)
Implementation of optimized ALCALE 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
wellbehaved (so called "nice") concepts and (2) implementation of the
socalled "lazy unfolding" of acyclic TBoxes. Both implementations
should then also be evaluated and compared.
Literature:
Tutor: AnniYasmin Turhan.
 (2) Semantic
Annotation of Webpages and description of the experiences made.

The semantic web is a current initiative for generating new
W3C standards that allow to
annotate WWW pages with a machineunderstandable description
of their content. Obviously, such a semantic annotation would
facilitate the implementation of more exact search engines
and allow the deployment of all kinds of autonomous agents
on the web. The purpose of this project is to semantically
annotate the web pages of the chair for automata theory using
the currently emerging OWL standard, and to
give a detailed discussion of the experiences made.
Literature:
 S. Bechhofer, L. Carr, C. Goble, S. Kampa, T. Milesboard.
The Semantics of Semantic Annotation. COHSE: Conceptual Open Hypermedia Service. Annotation for the Semantic Web eds. Siegfried Handschuh and Steffen Staab. IOS Press, Frontiers in Artifical Intelligence and Applications. Vol 96. 2003.
 S. Bechhofer,
I. Horrocks, C. Goble, and R. Stevens. OilEd: a reasonable
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 396408. SpringerVerlag, 2001.
Tutor: Carsten Lutz,
 (3)
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 AAAI99, 1999.
 I. Horrocks, P. F. PatelSchneider, and R. Sebastiani. An analysis
of empirical testing for modal decision procedures. Logic Journal
of the IGPL, 8(3):293323, 2000.
Tutor: Jan Hladik
 (4)
Implementation of a matching algorithm for the Description Logic ALN.
 A matching problem comprises a concept description and a
socalled 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
wellexamined this topic focusses on the implementation of the
relevant algorithm in LISP and on the evaluation w.r.t. runtime
behaviour.
Literature:
 F. Baader, R. Küsters, A. Borgida, and
D. McGuinness. Matching in Description Logics. Journal of Logic and
Computation, 9(3):411447, 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
 (5)
Unification in Equational Theories.
 An important problem in the area of Term Rewriting is
unification of two terms modulo an equational theory. This problem is
semidecidable
in general. There is a complete procedure to solve Eunification problems,
but this procedure does not halt for all inputs.
On the other hand, if we look for a solution with an equational proof of
a given length n and E is nonsubtermcollapsing,
then the Eunification procedure
becomes a decision procedure.
The project requires implementing the
procedure that takes as input an equational theory, a goal equation and
a natural number n, and gives as output
an equational proof of length n of the solved goal, if it exists, or
a negative answer if it does not exist.
Literature:
 B. Morawska. Completeness of Eunification with eager Variable Elimination.
LTCSReport 0303, Chair for Automata Theory, Institute for Theoretical
Computer Science,
Dresden University of Technology, Germany, 2003. See
http://lat.inf.tudresden.de/research/reports.html
Tutor: Barbara Morawska
Barbara Morawska