04. – 09. März 2001, Dagstuhl Seminar 01101



Ulrich Furbach (Universität Koblenz-Landau, DE)
Harald Ganzinger (MPI-SWS – Saarbrücken, DE)
Ryuzo Hasegawa (Kyushu University – Fukuoka, JP)
Deepak Kapur (University of New Mexico – Albuquerque, US)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team


Dagstuhl-Seminar-Report 300

Formal logic provides a mathematical foundation for many areas of computer science, including problem specification, program development, transformation, and verification, hardware design and verification, relational databases, knowledge engineering, theorem proving, computer algebra, logic programming, and artificial intelligence.

Using computers for solving problems in these areas, therefore, requires the design and implementation of algorithms based on logical deduction. It remains one of the great challenges in informatics to make computers capable of doing non-trivial logical reasoning, be it fully automatic, or in interaction with humans. Some progress, however, has been made in the past ten years: Bill McCune's program EQP has solved the Robbins algebra problem. Model checking, a form of theorem proving over finite models, has become a very successful push-button method for verifying combinatorially highly complex properties of both hardware and software. Methods of interactive theorem proving have helped in formally verifying semantic (type) safety aspects of programming languages such as Java.

The conviction that mathematical logic is a unifying principle in computer science and that methods from different theoretical areas as well as application domains should be brought together has lead to a successful new conference: FLoC, the Federated Logic Conferences, which was held in 1999 for the second time after its initiation in 1996.

Previous Dagstuhl seminars on automated deduction were held in 1993, 1995, 1997, and 1999. They were considered very successful in the way they stimulated research within the community. The 2001 seminar is intended to contribute to the interdisciplinary view of logic in computer science by bringing together leading scientists from various disciplines within the area of automated deduction, as well as from application areas, this time in particular from planning and program analysis and verification. Recent successes in the area of propositional satisfiability checking allow complex planning problems to be solved by deduction. Further improvements in the area might be possible if the view of predicate logic as schematic propositional logic is exploited and methods of automated theorem proving in first-order logic are integrated into satisfiability checkers. Program analysis and verification in the form of model checking or code certification are beginning to cross-fertilize each other. Firmly based on inter-related logic and algorithmic concepts, these areas are in the process of extending their scope from finite domain-based fixpoint computation to infinite systems where more complex forms of deductive computation are required, and where the gap to traditional forms of program verification based on induction needs to be closed.

We hope that you will accept the invitation to participate and to contribute to discussions that might help in transferring methods between subdiciplines as well as between theoretical research and application domains.

Dagstuhl Seminar Series


Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).


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).


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

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.