Jörg Denzinger's Home Page

Address:

Jörg Denzinger

AG Effiziente Algorithmen
Universität Kaiserslautern
Fachbereich Informatik
Postfach 3049
67653 Kaiserslautern, Germany

Tel: ++49 631 205 2181
Fax: ++49 631 205 3558

Email: denzinge@informatik.uni-kl.de

Gebäude 34, 414

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.

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

Deduction

Based on the DISCOUNT system, I have currently two projects (both funded by the DFG-Forschungsschwerpunkt ''Deduktion'', again). In the first one, Cooperation in Heterogeneous Theorem Prover Networks, we are interested in loosely coupling several theorem provers in order to achieve better results due to cooperation by exchanging results. In the second 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:

Program Committee Co-Chair: FLAIRS-97 Special Track on Using AI methods to control automated deduction
Co-Organizer: CADE-15 workshop on Using AI methods in Deduction
Program Committee Co-Chair: FLAIRS-99 Special Track on Parallel and Distributed Reasoning

Teaching Activities:

SS 98 :

Lecture: Distributed Knowledge-Based Search
Proseminar: Artificial Life with Prof. Avenhaus

WS 98/99 :

Lecture: Foundations of Evolutionary Algorithms
Training lecture: Learning Systems with colleagues from LSA

SS 99 :

Lecture: Foundations of Multi-Agent-Systems
Training lecture: Rewrite systems: Visualization of basic techniques with Java with Prof. Avenhaus

Publications online:

Avenhaus,J. ; Denzinger, J.: Distributing equational theorem proving, Proc. RTA'93, Montreal, LNCS 690, 1993, pp. 62-76.
Extended version as SEKI-Report SR-93-06, University of Kaiserslautern, 1993.
- Abstract
- Download full paper (88 Kbytes)
Sonntag,I. ; Denzinger, J.: Extending automatic theorem proving by planning, SEKI-Report SR-93-02, University of Kaiserslautern, 1993.
- Abstract
- Download full paper (106 Kbytes)
Denzinger,J. ; Fuchs, M. : Goal oriented equational theorem proving using team work, Proc. KI'94, Saarbrücken, LNAI 861, 1994, pp. 343-354.
Extended version as SEKI-Report SR-94-04, University of Kaiserslautern, 1994.
- Abstract
- Download full paper (85 Kbytes)
Denzinger,J. ; Schulz, S.: Analysis and Representation of Equational Proofs Generated by a Distributed Completion Based Proof System, SEKI-Report SR-94-05, University of Kaiserslautern, 1994.
- Abstract
- Download full paper (252 Kbytes)
Denzinger,J. ; Kronenburg, M.: Planning for distributed theorem proving: The team work approach, Proc. KI-96, Dresden, LNAI 1137, 1996, pp. 43-56.
Older version as SEKI-Report SR-94-09, University of Kaiserslautern, 1994.
- Abstract
- Download full paper (78 Kbytes)
Denzinger,J.: Completion and Equational Theorem Proving using Taxonomic Constraints, Proc. KI-96, Dresden, LNAI 1137, 1996, pp. 29-42.
Extended version as SEKI-Report SR-95-11, University of Kaiserslautern, 1995.
- Abstract
- Download full paper (70 Kbytes)
Denzinger, J. ; Fuchs, M. : Experiments in Learning Prototypical Situations for Variants of the Pursuit Game, Proc. 2nd ICMAS, Kyoto, AAAI Press, 1996, pp. 48-55.
Extended version as LSA-Report LSA-96-04E, University of Kaiserslautern, 1996.
- Download full paper (75 Kbytes)
Denzinger, J. ; Fuchs, Matt. ; Fuchs, Marc: High Performance ATP Systems by Combining Several AI Methods, Proc. IJCAI-97, Morgan Kaufmann, 1997, pp. 102-107.
Extended Version as SEKI-Report SR-96-09, University of Kaiserslautern, 1996.
- Abstract
- Download full paper (97 Kbytes)
Denzinger, J. ; Fuchs, D.: Cooperation in Theorem Proving by Loosely Coupled Heuristics, SEKI-Report SR-97-03, University of Kaiserslautern, 1997.
- Abstract
- Download full paper (101 Kbytes)
Denzinger, J. ; Scholz, S.: Using Teamwork for the Distribution of Approximately Solving the Traveling Salesman Problem with Genetic Algorithms, SEKI-Report SR-97-04, University of Kaiserslautern, 1997.
- Abstract
- Download full paper (109 Kbytes)
Denzinger, J. ; Fuchs, D.: Knowledge-based Cooperation between Theorem Provers by TECHS, SEKI-Report SR-97-11, University of Kaiserslautern, 1997. Algorithms, SEKI-Report SR-97-04, University of Kaiserslautern, 1997.
- Abstract
- Download full paper (80 Kbytes)