February 28 – March 5 , 1999, Dagstuhl Seminar 99091



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

For support, please contact

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 the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.