Dagstuhl Seminar 07401
Deduction and Decision Procedures
( Sep 30 – Oct 05, 2007 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/07401
Organizers
- Franz Baader (TU Dresden, DE)
- Byron Cook (Microsoft Research UK - Cambridge, GB)
- Jürgen Giesl (RWTH Aachen, DE)
- Robert Nieuwenhuis (UPC - Barcelona, ES)
Contact
- Annette Beyer (for administrative matters)
Impacts
- LTL over description logic axioms : article in KR 2008 (Proceedings of the eleventh international conference on principles of knowledge representation and reasoning) : S. 684 - 694 - Franz Baader ; Silvio Ghilardi ; Carsten Lutz - Menlo Park : AAAI Press, 2008. - S. 684-694 - (Proceedings of the eleventh international conference on principles of knowledge representation and reasoning : S. 684-694).
- LTL over description logic axioms : article in Proceedings ot the 21st international workshop on description logics : DL 2008, Dresden, Germany, May 13 - 16, 2008 - Franz Baader ; Silvio Ghilardi ; Carsten Lutz - Dresden : Universität , 2008.
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.
- Markus Aderhold (TU Darmstadt, DE)
- Franz Baader (TU Dresden, DE) [dblp]
- Domagoj Babic (Synopsys Inc. - Mountain View, US)
- Peter Baumgartner (NICTA - Canberra, AU) [dblp]
- Bernhard Beckert (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Marc Bezem (University of Bergen, NO)
- Aaron Bradley (University of Colorado - Boulder, US)
- Sergiu Bursuc (University of Birmingham, GB)
- Alessandro Cimatti (Bruno Kessler Foundation - Trento, IT) [dblp]
- Koen Claessen (Chalmers UT - Göteborg, SE) [dblp]
- Leonardo de Moura (Microsoft Research - Redmond, US) [dblp]
- Germain Faure (UPC - Barcelona, ES)
- Alexander Fuchs (University of Iowa - Iowa City, US)
- Silvio Ghilardi (University of Milan, IT) [dblp]
- Jürgen Giesl (RWTH Aachen, DE) [dblp]
- Reiner Hähnle (TU Darmstadt, DE) [dblp]
- Thomas Hillenbrand (MPI für Informatik - Saarbrücken, DE)
- Jochen Hoenicke (Universität Freiburg, DE)
- Dieter Hutter (DFKI - Saarbrücken, DE)
- Deepak Kapur (University of New Mexico - Albuquerque, US) [dblp]
- Laura Kovács (TU Wien, AT) [dblp]
- Sava Krstic (Intel Corp. - Hillsboro, US)
- Viktor Kuncak (EPFL - Lausanne, CH) [dblp]
- Temur Kutsia (Universität Linz, AT)
- Christopher Lynch (Clarkson University - Potsdam, US) [dblp]
- Aart Middeldorp (Universität Innsbruck, AT) [dblp]
- Enrica Nicolini (CNRS - Nancy, FR)
- Ilkka Niemelä (Helsinki University of Technology, FI)
- Robert Nieuwenhuis (UPC - Barcelona, ES) [dblp]
- Tobias Nipkow (TU München, DE) [dblp]
- Claudia Obermaier (Universität Koblenz-Landau, DE)
- Albert Oliveras (Polytechnic University of Catalonia, ES) [dblp]
- Ruzica Piskac (EPFL - Lausanne, CH) [dblp]
- Andreas Podelski (Universität Freiburg, DE) [dblp]
- Christophe Ringeissen (LORIA - Nancy, FR) [dblp]
- Enric Rodríguez-Carbonell (UPC - Barcelona, ES) [dblp]
- Albert Rubio (UPC - Barcelona, ES) [dblp]
- Philipp Rümmer (University of Oxford, GB) [dblp]
- Andrey Rybalchenko (TU München, DE) [dblp]
- Renate Schmidt (University of Manchester, GB) [dblp]
- Manfred Schmidt-Schauss (Goethe-Universität - Frankfurt a. M., DE) [dblp]
- Peter Schneider-Kamp (University of Southern Denmark - Odense, DK) [dblp]
- Stephan Schulz (TU München, DE) [dblp]
- Roberto Sebastiani (Università di Trento, IT) [dblp]
- Viorica Sofronie-Stokkermans (MPI für Informatik - Saarbrücken, DE) [dblp]
- Ofer Strichman (Technion - Haifa, IL) [dblp]
- Pierre-Yves Strub (Ecole Polytechnique - Palaiseau, FR) [dblp]
- René Thiemann (Universität Innsbruck, AT) [dblp]
- Cesare Tinelli (University of Iowa - Iowa City, US) [dblp]
- Andrei Voronkov (University of Manchester, GB) [dblp]
- Uwe Waldmann (MPI für Informatik - Saarbrücken, DE) [dblp]
- Christoph Walther (TU Darmstadt, DE)
- Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
- Volker Weispfenning (Universität Passau, DE)
- Calogero G. Zarba (Universität des Saarlandes, DE)
Related Seminars
- Dagstuhl Seminar 9310: Deduction (1993-03-08 - 1993-03-12) (Details)
- Dagstuhl Seminar 9512: Deduction (1995-03-20 - 1995-03-24) (Details)
- Dagstuhl Seminar 9709: Deduction (1997-02-24 - 1997-02-28) (Details)
- Dagstuhl Seminar 99091: Deduction (1999-02-28 - 1999-03-05) (Details)
- Dagstuhl Seminar 01101: Deduction (2001-03-04 - 2001-03-09) (Details)
- Dagstuhl Seminar 03171: Deduction and Infinite-state Model Checking (2003-04-21 - 2003-04-25) (Details)
- Dagstuhl Seminar 05431: Deduction and Applications (2005-10-23 - 2005-10-28) (Details)
- Dagstuhl Seminar 09411: Interaction versus Automation: The two Faces of Deduction (2009-10-04 - 2009-10-09) (Details)
- Dagstuhl Seminar 13411: Deduction and Arithmetic (2013-10-06 - 2013-10-11) (Details)
- Dagstuhl Seminar 15381: Information from Deduction: Models and Proofs (2015-09-13 - 2015-09-18) (Details)
- Dagstuhl Seminar 17371: Deduction Beyond First-Order Logic (2017-09-10 - 2017-09-15) (Details)
- Dagstuhl Seminar 19371: Deduction Beyond Satisfiability (2019-09-08 - 2019-09-13) (Details)
- Dagstuhl Seminar 21371: Integrated Deduction (2021-09-12 - 2021-09-17) (Details)
- Dagstuhl Seminar 23471: The Next Generation of Deduction Systems: From Composition to Compositionality (2023-11-19 - 2023-11-24) (Details)
- Dagstuhl Seminar 26091: Revisiting the Foundations of Deduction in a New World (2026-02-22 - 2026-02-27) (Details)
Classification
- artificial intelligence / robotics
- semantics / specification /formal methods
- verification / logic
Keywords
- automated deduction
- decision procedures
- verfication and specification
