Research fields

Most of the research done in our group is concerned with automated deduction, that is, with the problem of how to automate the process of drawing logical inferences. In this context, we are mainly interested in subclasses of first-order predicate logic for which the interesting inference problems are still decidable. On one hand, we are investigating the combination of special deduction methods, and their integration into general deduction procedures. On the other hand, we are designing logic-based knowledge representation languages with decidable inference problems.

Deduction

Within the research area of deduction we are interested in automatic theorem proving, term rewriting, and unification.

In particular, we turned our attention to the integration of special deduction methods (see completed research project Combination of Specific Deduction Procedures): When solving logical inference problems, one can choose between two fundamentally different ways of proceeding. On one hand, one can try to design special inferences methods that are tailored to a particular class of inference problems. These methods are usually rather efficient, but they only apply to the restricted class they have been designed for. On the other hand, one can try to apply general purpose deduction procedures (such as resolution-based theorem proving or Knuth-Bendix completion). The integration of special inference methods into general purpose deductive systems aims at a combination of the efficiency of the special method with the universality of the general method. In this context, one is faced with the problems of how to combine a special inference method with a general purpose inference procedure, and of how to combine different special inference methods with each other. Combination problems of the second kind have already been investigated in depth for the combination of algorithm for unification modulo equational theories over disjoint signatures.

Knowledge representation

Terminological knowledge representation (KR) languages have been developed as a structured formalisms for representing of the taxonomic knowledge of a given application domain. Terminological knowledge representation systems are, for example, applied in natural language processing, in automated planning systems, and for supporting configuration of technical systems. An important point in favour of terminological KR languages is that they are equipped with a clear and formally well-understood logic-based semantics.

On one hand, this formalization shows that terminological KR languages can be viewed as subclasses of first order predicate logic. From an algorithmic point of view it is important that many of the languages considered until now yield decidable subclasses of first order predicate logic, which are not contained in one of the well-known decidable fragments. For these languages, decision procedures have been developed that are based on the well-known tableaux calculus for predicate logic. Interestingly, this approach usually yields procedures that are optimal with respect to worst case complexity of the respective inference problem.

On the other hand, the formal semantics provides us with an implementation-independent description of the behaviour of a terminological system. This improves the transparency for the user of such a system, and it facilitates comparing different systems.

Computing with Molecules

Different ideas for development of unconventional models for computation were discussed and realized during the last years. Some of these developments are based on abstractions of molecular biological processes (e.g. recombination) for application in mathematics and computer science. The resulting models for computation supplement their classical counterparts from theoretical computer science. Molecules of DNA (deoxyribonucleic acid) serve as data carrier and as storage medium for information. Suitable molecular biological reactions and processes on DNA are used as operations. Research activities aim to construct a model for a universal biological computer that can be implemented in a molecular biological laboratory. Algorithms for biological computers particularly feature by massive data parallelism and high computational speed leading to a challenge for the electronic state of the art technology. Research topics:

• Universal Distributed Splicing Systems
• Simulation Systems for Molecular Biological Processes on DNA
• DNA Based Algorithmic Design