Formale Methoden und Deduktion Prof. Dr. J. Avenhaus

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.

Deduction

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:

• 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
• Organizing Committee Chair: AAAI-2000 workshop on Parallel and Distributed Search for Reasoning

Teaching Activities:

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

WS 99/00 :

• Lecture: Distributed Knowledge-Based Search

Publications

Last Change: 20/07/2000

Impressum

AG Formale Methoden und Deduktion

Fachbereich Informatik

Technische Universität Kaiserslautern