The project group is offered for students of Computational Logic (Master, module MCL-P).
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
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
Knowledge from the lectures Formale Systeme, Theoretische Informatik und Logik,
and Descriptions Logics is helpful.
(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
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
This project requires basic knowledge about
first-order logic and good programming skills.
(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
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.
(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.
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.
(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 . 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 .
Working on this project would require basic knowledge of description logics and
good programming skills in Java.