Komplexpraktikum/Project "Automated Reasoning in Logical Formalisms" in WS 2004/05

Initial meeting

takes place on October 12th at 14:50 (5. DS) in Room 356. 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 October 11.

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. 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.

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 team-working 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.

It is also the duty of the participants to reserve enough time for performing the project. The sharp deadline for finishing the project is the beginning of the following semester, i.e. the allowed time for the project is one semester plus the following semester break. Failure to finish the project in time will result in no credits to be given. It is the obligation of the participant to start the project in time, and to make appointsments with the supervisor for regular meetings during the semester.

Topics

When choosing a topic, please take into account the knowledge you have already acquired. For example, if you'd like to do a project concerning knowledge representation, you are expected to have sucessfully attended the lecture "Logic-based knowledge representation" before starting the project.

(1) Implementation of most specific concept

"Most specific concept" (msc) is a new reasoning service for description logics. So far no implementation of this reasoning service exists. The purpose of this project is to implement the msc for the description logics EL and then to extend it to ALE. The implementation should then also be evaluated.

Literature:

• R. Küsters and R. Molitor, "Approximating Most Specific Concepts in Description Logics with Existential Restrictions".
• R. Küsters and R. Molitor, "Computing Most Specific Concepts in Description Logics with Existential Restrictions".
• Guy L., Jr. Steele, "Common Lisp: The Language".

Prerequisites: Lecture "Logic-based Knowledge Representation" and basic skills in the programming language LISP

Tutor: Anni-Yasmin Turhan.

(2) Implementation of Tools for the Term Rewriting lecture.

The project consists of finding appropriate tools which can help in learning concepts presented in the Term Rewriting lecture and installing them (under supervision). The main systems designed for the problems in term rewriting can be found at http://rewriting.loria.fr.

A student will have to choose appropriate systems, get to know their functionality and design a common interface. The main problems which should be possible to solve with the help of the existing tools are:

• with a TRS and a term as an input, output a normal form of the term or a set of its normal forms;
• with a TRS as an input, decide its termination using the orders known from the lecture (lpo, polynomial order);
• with an equational theory as an input, perform its completion.

Since different systems may have different input/output formats, the decision should be made on one such format, which is then translated depending on which system is going to be used to solve a specific problem. A short manual should be written describing how to use the tools for term rewriting, i.e. how to write correct input, how to trigger a desirable action and what is the form of the output.

Literature:

• Database of Rewriting Systems, http://rewriting.loria.fr/
• Franz Baader, Tobias Nipkow. Term Rewriting and All That, Cambridge University Press, 1998.

Prerequisites: Lecture "Term Rewriting Systems"

Tutor: Barbara Morawska,

(3) Threshold of satisfiability of description logics.

Many logical problems show a 0-1 law or threshold property: below a given value of a parameter of the problem almost all inputs are satisfiable, beyond almost all are unsatisfiable, and around this value, the threshold, most solvers are much slower than away from the threshold. The goal of this project is to investigate parameters for different DLs by empirical observation. This will be accomplished by creating a generator of DL formulas under varying parameters, running experiments (testing for satisfiability using a DL solver), and organizing the results.

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.

Prerequisites: Lecture "Logic-based Knowledge Representation"

Tutor: Mitch Harris

(4) Reasoning about Semantic Web Services.

The declarative description of the behavior of services offered on the world wide web is an emerging research area. A recent proposal suggests a framework for representing web services that is based on description logics. It is shown that reasoning in this framework can be reduced to standard description logic reasoning tasks. The goal of the project is to implement the existing translation from reasoning with web services to reasoning in description logics, such that existing description logic reasoners (e.g., the RACER system) can be used to reason about web services. One complication to be solved is that the translation introduces so-called nominals which cannot be processed by current reasoners and need, in turn, to be "translated" in an appropriate way.

Literature:

• C. Lutz and U. Sattler. A Proposal for Describing Services with DLs. In Proceedings of the 2002 International Workshop on Description Logics, 2002.
• More will be provided.

Prerequisites: Lecture "Logic-based Knowledge Representation"

Tutor: Carsten Lutz