28. Februar – 05. März 1999, Dagstuhl-Seminar 99091



U. Furbach (Koblenz), H. Ganzinger (MPI-Saarbrücken), D. Kapur (Albany)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl-Seminar-Report 232


Logic has become a prominent formal language and formalism for all of computer science. It serves in many applications such as in problem specification, program development, program transformation, program verification, hardware design and verification, consistency checking of databases, theorem proving, expert systems, logic programming, and so on and so forth. Its strength derives from the universality of the language as well as from the fundamental logical operations and relations. Logical manipulations as needed in all these applications are realized by mechanisms developed in the field of deduction which has produced a variety of techniques of great importance in all these applications.

All these research issues are subject of a "Schwerpunktprogramm Deduktion'' funded by the Deutsche Forschungsgemeinschaft.

During the last years successful research in this program has led to the development of high performance deduction systems, and to laying a broad basis for various applications.

This success of deduction can be observed within the international AI and computer science scene as well. Deduction systems recently have achieved considerable successes and even public press: it was a first-order theorem prover which first proved the Robbins algebra conjecture and even reached the New York Times Science section. But not only in proofing mathematical theorems, also in various other disciplines of AI, automated deduction made substantial progress. In planning, for example, it turned out that propositional theorem provers are able to outperform special purpose planning systems. This is remarkable, since it was considered folklore that planning requires specialized algorithms, which was only recently disproved by the development of propositional satisfiability testing methods which can now handle much larger planning problem sizes. A very similar development can be observed in the field of model based diagnosis.

It is the idea of the proposed Dagstuhl-Seminar to bring together leading scientists in the area of Deduction from all over the world. By all participants the previous seminars in 1993, 1995 and 1997 were unanimously considered great successes and rated as top quality w.r.t. the scientific contributions presented in the talks. The quality is also reflected in the Dagstuhl-Seminar Reports No. 58, 110 and 170 of these seminars. Due to this outstanding success and to the growing importance of deduction the seminar will be held again.

A particular interest will be put on the application of deduction within AI systems and in general in software development.

Dagstuhl-Seminar Series


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.