Project Group

Technische Universität Dresden Institut für Theoretische Informatik Lehrstuhl für Automatentheorie

Prof. Dr.-Ing. Franz Baader

The project group is offered for students of Computational Logic (Master, module MCL-P).

Organisation

The initial meeting takes place on April 24 at 15:15 in room APB/3027. Students who are not able to attend the initial meeting please contact Francesco Kriegel before April 23.
The participants are expected to read the relevant literature, and to discuss it with their tutor in order to become acquainted with the chosen topic. The required implementation work (if any) 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 deadline for finishing the project is the end of the semester (exam period), i.e. the allowed time for the project is one semester plus the 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 appointments with the supervisor for regular meetings during the semester.
Knowledge from the lectures Formale Systeme, Theoretische Informatik und Logik, and Descriptions Logics is helpful.

Topics

(1) Finite Herbrand Models for Horn Clauses

Deciding the existence of finite Herbrand models for certain sets of first-order anti-Horn clauses is ExpTime-complete. The aim of this project is to analyze the computational complexity of the same problem for Horn clauses by finding a hardness proof and/or a decision procedure.

This project requires basic knowledge about first-order logic and complexity theory.

References
[1] Report: http://lat.inf.tu-dresden.de/research/papers/2012/BoMo-LPAR-12.pdf

Tutor: Stefan Borgwardt

(2) Finite Herbrand Models for anti-Horn Clauses

The aim of this project is to implement and optimize an algorithm for deciding the existence of finite Herbrand models for certain sets of first-order anti-Horn clauses. The program should be evaluated on a representative set of input problems. The programming language can be chosen by the student.

This project requires basic knowledge about first-order logic and good programming skills.

References
[1] Report: http://lat.inf.tu-dresden.de/research/papers/2012/BoMo-LPAR-12.pdf

Tutor: Stefan Borgwardt

(3) Most Specific Generalizations w.r.t. General TBoxes in ELgfp

This project aims at the implementation and evaluation of methods for calculating least common subsumers and most specific concepts in the leight-weight description logic ELgfp, i.e. EL interpreted with greatest fixpoint semantics. In contrast to standard EL with descriptive semantics, those most specific generalizations always exist in ELgfp and can be computed in polynomial time. Furthermore, the student should make a comparison with most specific generalizations w.r.t. standard descriptive semantics and with role-depth bounded most specific generalizations w.r.t. descriptive semantics.

Basic knowledge in description logics and good programming skills are expected. For an easier handling and integration with existing software (e.g. Elk, Protege etc.), the program should be built on top of the OWL API.

References
[1] Franz Baader: Least Common Subsumers and Most Specific Concepts in a Description Logic with Existential Restrictions and Terminological Cycles
[2] OWL API

Tutor: Francesco Kriegel

(4) Formal Concept Analysis & Propositional Logic: From Pseudo-Intents to Implicational Bases

This project's aim is the formulation of a minimal theory of implications, which holds in a given set of propositional models and furthermore entails all other implications, that hold in the given model set. This requires an isomorphism between propositional model sets and formal contexts, to adapt the existing results for implicational bases of formal contexts. Furthermore the student should give an algorithm to compute the implicational base. The results can be extended to propositional bases.

Basic knowledge in propositional logic and set theory is expected. Further knowledge in logic or order theory may be helpful.

References
[1] Bernhard Ganter and Rudolf Wille: Formal Concept Analysis, ISBN 3-540-62771-5, Springer Verlag
[2] Bernhard Ganter: Attribute Exploration with Background Knowledge

Tutor: Francesco Kriegel

(5) Unification in Description Logics

The system UEL can be used to detect redundancies in ontologies by trying to unify concepts formulated in the description logic EL. The goal of this project is the implementation of a newly developed rule-based algorithm that allows to take into account negative constraints during unification.

This project requires basic knowledge about description logics and good programming skills.

References
[1] UEL: http://uel.sourceforge.net/
[2] Report: http://lat.inf.tu-dresden.de/research/reports/2015/BaBM-LTCS-15-03.pdf

Tutor: Stefan Borgwardt

(6) Extending a Tool for Computing Logical Differences

The aim of this project is to extend a new tool for detecting logical differences between ontologies based on a hypergraph representation of ontologies [2]. The tool should be extended in such a way that not only differences w.r.t. concept subsumption queries, but also regarding instance & conjunctive queries can be found. Moreover, ontologies formulated in EL extended with role inclusions, and domain & range restrictions should be accepted as input. A description of the extended algorithms is available in [1].

Working on this project would require basic knowledge of description logics and good programming skills in Java.

Literatur
[1] http://dx.doi.org/10.3233/978-1-61499-419-0-555
[2] http://lat.inf.tu-dresden.de/research/papers/2013/EcLuWa-DChanges2013.pdf

Tutor: Michel Ludwig

More topics t.b.a.