https://www.dagstuhl.de/07401

September 30 – October 5 , 2007, Dagstuhl Seminar 07401

Deduction and Decision Procedures

Organizers

Franz Baader (TU Dresden, DE)
Byron Cook (Microsoft Research UK – Cambridge, GB)
Jürgen Giesl (RWTH Aachen, DE)
Robert Nieuwenhuis (UPC – Barcelona, ES)

For support, please contact

Dagstuhl Service Team

Documents

Dagstuhl Seminar Proceedings DROPS
List of Participants
Dagstuhl's Impact: Documents available

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. Significant progress, however, has been made in the past ten years. For example, real arithmetic algorithms in Intel processors were formally verified using an interactive theorem prover, interactive and automatic theorem provers are routinely used in formal methods tools, and automatic theorem provers and finite model building programs solved various open mathematical problems of combinatorial nature. Automated deduction, in particular for socalled 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 from 1992 to 1998 together with the seven previous Dagstuhl seminars on "Deduction" (held biennially since 1993) have been instrumental in obtaining these successes.

Because of the recent progress in applying automated deduction methods and tools in various application areas, like hardware and software verification, cryptographic protocols, programming languages, and the semantic web, the focus of the Deduction seminar in 2005 was on applications of deduction. The application areas best represented at that seminar (in terms of number of talks held) concerned various forms of "verification." From the talks on these applications, it became clear that the integration of theory specific reasoners, in particular decision procedures, into a core general purpose verification environment and the exible and semantically well-founded combination of such reasoners are extremely important in many applications of verification tools.

For this reason, the focus of the Deduction seminar in 2007 was on decision procedures and their integration into general purpose theorem provers. Our goal was to further the confluence between application-driven approaches for combining and using decision procedures in deduction and the strong foundational research on this topic.

In total we had 55 participants, mostly from Europe, but also from USA, Israel, and Australia. A good balance between more senior and junior participants was maintained. The program consisted of 37 relatively short talks, which gave ample time for discussion, both during and after the talks.

The talks and discussions showed that "Deduction and Decision Procedures" is currently a very important and vibrant research area, which creates both important new foundational results and tools that are at the core of recent advances in various subareas of "verification." The approach most strongly represented at the seminar was the SMT (Satisfiability Modulo Theories) approach, a trend that was already discernible during the 2005 Seminar on "Deduction and Applications," but has become even stronger in the last two years.

The seminar showed that there are essentially three different approaches for using deduction in program verification: (1) extremely powerful interactive theorem provers which however lack the necessary automation, (2) automated theorem provers mainly based on first-order logic which however fail to cater for important aspects like arithmetic, and (3) specialized tools like SMT solvers based on powerful automatic procedures for particular logical theories. These three approaches have all led to impressive results in the last years. However, the communities working on these approaches are still unnecessarily disjoint. Therefore, the seminar revealed that a main goal for the future of deduction is to improve the collaboration and the combination of interactive and automated deduction (both for first-order logic and for SMT). For this reason, the next Deduction seminar (planned for 2009) will focus on "Interaction vs. Automation: The two Faces of Deduction".

The seminar consisted of a full, but not overly loaded program which left enough time for discussions.We felt the atmosphere to be very productive, characterized by many discussions, both on-line during the talks and off-line during the meals and in the evenings. Altogether, we perceived the seminar as a very successful one, which gave the participants an excellent opportunity to get an overview of the state-of-the-art concerning decision procedures in automated deduction and their applications in areas related to verification. The seminar has further enhanced the cross-fertilization between foundational research on this topic and application-driven approaches.

Dagstuhl Seminar Series

Classification

  • Artificial Intelligence / Robotics
  • Semantics / Specification /formal Methods
  • Verification / Logic

Keywords

  • Automated deduction
  • Decision procedures
  • Verfication and specification

Book exhibition

Books from the participants of the current Seminar 

Book exhibition in the library, ground floor, during the seminar week.

Documentation

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

Publications

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

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.

NSF young researcher support