Formale Methoden und Deduktion
Prof. Dr. J. Avenhaus

FB Inf

Jörg Denzinger


Jörg Denzinger

AG Formale Methoden und Deduktion
Technische Universität Kaiserslautern
Fachbereich Informatik
Postfach 3049
67653 Kaiserslautern, Germany

Fax: ++49 631 205 2156


Research Projects:

My main interest is distributed knowledge-based search, i.e. search processes that use knowledge to control their steps and that are distributed among several computers of a local network. Since search is only a fundamental technique it has to be applied to some problems. The problems that interest me involve also methods from other areas of artificial intelligence, like learning, planning, deduction or multi-agent systems.

Distributed knowledge-based search

I developed the teamwork method for search processes that use sets of facts as state representations and heuristics to choose among the many possible transitions between states. In the project distributed, knowledge-based theorem proving, funded by the DFG-Forschungsschwerpunkt ''Deduktion'', we examined teamwork with regards to automated theorem proving, namely generating theorem provers. Within this project we developed the DISCOUNT system.

We also used the teamwork method in distributed systems for solving the traveling salesman problem and for generating time tables (both on basis of genetic algorithms).

Based on our experience with teamwork we developed the TECHS approach for heterogeneous, distributed, knowledge-based search. TECHS allows the cooperation of different search processes without limitations on the state representations these processes use. In the project Cooperation in Heterogeneous Theorem Prover Networks (funded by the DFG-Forschungsschwerpunkt ''Deduktion'', again), we employed TECHS in the area of automated deduction. In the project Cooperation of Heterogeneous Search Mechanisms (funded by the DFG) we try to improve on the first TECHS project in the area of automated deduction and we also applied TECHS in the area of optimization problems, namely for job-shop scheduling.


Based on the DISCOUNT system, I had an additional project funded by the DFG-Forschungsschwerpunkt ''Deduktion''. In this project, LEASH (LEArning of Search Heuristics for theorem proving), we use teamwork as the basis to solve the various problems that occur, when using learned knowledge in theorem provers.

Multi-agent systems

In the EPIN project (Evolution of Prototypical INstances) (see our report) we investigate how reactive behaviour of agents can be automatically learned. We are especially interested in learning agents that have to cooperate with each other in order to achieve a given goal. Basis of our approach is an agent model that uses (prototype situation/action)-pairs together with the Nearest Neighbour Rule as decision procedure. By employing (knowledge-based) search among the possible sets of pairs we can evolve appropriate agents for a given task.

Organisational Activities:

Teaching Activities:

WS 98/99 :

SS 99 :

WS 99/00 :


For more publications of our group regarding my research interests please visit either the publications of our group or the teamwork bibliography.

Last Change: 20/07/2000

Impressum AG Formale Methoden und Deduktion Fachbereich Informatik Technische Universität Kaiserslautern Valid HTML 4.01!

Letzte Änderung: Wednesday, 26-Oct-05 08:59:20 GMT