http://www.dagstuhl.de/05431

23. – 28. Oktober 2005, Dagstuhl Seminar 05431

Deduction and Applications

Organisatoren

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)

Auskunft zu diesem Dagstuhl Seminar erteilt

Dagstuhl Service Team

Dokumente

Dagstuhl Seminar Proceedings DROPS
Teilnehmerliste

Summary

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

Buchausstellung

Bücher der Teilnehmer 

Buchausstellung im Erdgeschoss der Bibliothek

(nur in der Veranstaltungswoche).

Dokumentation

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

Publikationen

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.