October 23 – 28 , 2005, Dagstuhl Seminar 05431

Deduction and Applications


Franz Baader (TU Dresden, DE)
Peter Baumgartner (MPI für Informatik – Saarbrücken, DE)
Robert Nieuwenhuis (UPC – Barcelona, ES)
Andrei Voronkov (University of Manchester, GB)

For support, please contact

Dagstuhl Service Team


Dagstuhl Seminar Proceedings DROPS
List of Participants


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 perform non-trivial logical reasoning, be it fully automatic, or in interaction with humans. Some progress, however, has been made in the past ten years:

  • Automated theorem provers and finite model building programs solved various open mathematical problems of combinatorial nature.
  • Model checking, a form of theorem proving over finite models, has become a very successful push-button method for verifying nontrivial safety properties of hardware and software.
  • Automated deduction, in particular for so-called description logics, is widely assessed as a core enabling technology for the Semantic Web .
  • Methods of interactive theorem proving have helped in formally verifying semantic (type) safety aspects of programming languages such as Java. The "Schwerpunktprogramm Deduktion " funded by the Deutsche Forschungsgemeinschaft together with previous Dagstuhl seminars on "Deduction" have been instrumental in obtaining these successes.

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 as a means to fight fragmentation has lead to successful new conferences like FLoC and IJCAR, and to IFCoLoG, the recently established International Federation for Computational Logic.

This interdisciplinary view of logic in computer science motivated the Dagstuhl seminar. Specifically, we considered several application areas:

  • Software verification
  • Hardware verification
  • Cryptographic protocols
  • Programming languages
  • Formal methods
  • Semantic Web
  • Large knowledge bases.

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.