30. September – 05. Oktober 2007, Dagstuhl Seminar 07401
Deduction and Decision Procedures
Auskunft zu diesem Dagstuhl Seminar erteilt
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
- 17371: "Deduction Beyond First-Order Logic" (2017)
- 15381: "Information from Deduction: Models and Proofs" (2015)
- 13411: "Deduction and Arithmetic" (2013)
- 09411: "Interaction versus Automation: The two Faces of Deduction" (2009)
- 05431: "Deduction and Applications" (2005)
- 03171: "Deduction and Infinite-state Model Checking" (2003)
- 01101: "Deduction" (2001)
- 99091: "Deduction" (1999)
- 9709: "Deduction" (1997)
- 9512: "Deduction" (1995)
- 9310: "Deduction" (1993)
- Artificial Intelligence / Robotics
- Semantics / Specification /formal Methods
- Verification / Logic
- Automated deduction
- Decision procedures
- Verfication and specification