Dagstuhl Seminar 01101
Deduction
( Mar 04 – Mar 09, 2001 )
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/01101
Organizers
- Ulrich Furbach (Universität Koblenz-Landau, DE)
- Harald Ganzinger (MPI-SWS - Saarbrücken, DE)
- Ryuzo Hasegawa (Kyushu University - Fukuoka, JP)
- Deepak Kapur (University of New Mexico - Albuquerque, US)
Contact
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 capable of doing non-trivial logical reasoning, be it fully automatic, or in interaction with humans. Some progress, however, has been made in the past ten years: Bill McCune's program EQP has solved the Robbins algebra problem. Model checking, a form of theorem proving over finite models, has become a very successful push-button method for verifying combinatorially highly complex properties of both hardware and software. Methods of interactive theorem proving have helped in formally verifying semantic (type) safety aspects of programming languages such as Java.
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 has lead to a successful new conference: FLoC, the Federated Logic Conferences, which was held in 1999 for the second time after its initiation in 1996.
Previous Dagstuhl seminars on automated deduction were held in 1993, 1995, 1997, and 1999. They were considered very successful in the way they stimulated research within the community. The 2001 seminar is intended to contribute to the interdisciplinary view of logic in computer science by bringing together leading scientists from various disciplines within the area of automated deduction, as well as from application areas, this time in particular from planning and program analysis and verification. Recent successes in the area of propositional satisfiability checking allow complex planning problems to be solved by deduction. Further improvements in the area might be possible if the view of predicate logic as schematic propositional logic is exploited and methods of automated theorem proving in first-order logic are integrated into satisfiability checkers. Program analysis and verification in the form of model checking or code certification are beginning to cross-fertilize each other. Firmly based on inter-related logic and algorithmic concepts, these areas are in the process of extending their scope from finite domain-based fixpoint computation to infinite systems where more complex forms of deductive computation are required, and where the gap to traditional forms of program verification based on induction needs to be closed.
We hope that you will accept the invitation to participate and to contribute to discussions that might help in transferring methods between subdiciplines as well as between theoretical research and application domains.
- Jürgen Avenhaus (TU Kaiserslautern, DE)
- David Basin (ETH Zürich, CH) [dblp]
- Peter Baumgartner (MPI für Informatik - Saarbrücken, DE) [dblp]
- Bernhard Beckert (Universität Koblenz-Landau, DE) [dblp]
- Stefan Berghofer (TU München, DE)
- Wolfgang Bibel (TU Darmstadt, DE)
- Maria Paola Bonacina (University of Verona, IT) [dblp]
- Hans de Nivelle (MPI für Informatik - Saarbrücken, DE) [dblp]
- Ulrich Furbach (Universität Koblenz-Landau, DE) [dblp]
- Harald Ganzinger (MPI-SWS - Saarbrücken, DE)
- Martin Giese (Chalmers UT - Göteborg, SE) [dblp]
- Jürgen Giesl (RWTH Aachen, DE) [dblp]
- Rajeev P. Gore (Australian National University, AU) [dblp]
- Reiner Hähnle (Chalmers UT - Göteborg, SE) [dblp]
- Steffen Hölldobler (TU Dresden, DE) [dblp]
- Ian Horrocks (University of Manchester, GB) [dblp]
- Ullrich Hustadt (University of Liverpool, GB) [dblp]
- Dieter Hutter (DFKI - Saarbrücken, DE)
- Katsumi Inoue (National Institute of Informatics - Tokyo, JP) [dblp]
- Mitsuru Ishizuka (University of Tokyo, JP)
- Deepak Kapur (University of New Mexico - Albuquerque, US) [dblp]
- Manfred Kerber (University of Birmingham, GB)
- Claude Kirchner (LORIA & INRIA - Nancy, FR) [dblp]
- Michael Kohlhase (Jacobs Universität - Bremen, DE) [dblp]
- Alexander Leitsch (TU Wien, AT) [dblp]
- Reinhold Letz (TU München, DE)
- Donald W. Loveland (Duke University - Durham, US)
- Michael Lowry (NASA / RIACS - Moffett Field, US) [dblp]
- Christopher Lynch (Clarkson University - Potsdam, US) [dblp]
- Fabio Massacci (Università di Trento, IT) [dblp]
- Olga Shumsky Matlin (Northwestern University - Evanston, US)
- David McAllester (TTIC - Chicago, US)
- William McCune (Argonne National Laboratory, US)
- Erica Melis (DFKI - Saarbrücken, DE)
- Paliath Narendran (University of Albany - SUNY, US)
- Robert Nieuwenhuis (UPC - Barcelona, ES) [dblp]
- Hans-Jürgen Ohlbach (LMU München, DE)
- Jens Otten (TU Darmstadt, DE) [dblp]
- Brigitte Pientka (McGill University - Montreal, CA) [dblp]
- David A. Plaisted (University of North Carolina at Chapel Hill, US)
- Alexandre Riazanov (University of Manchester, GB)
- Renate Schmidt (University of Manchester, GB) [dblp]
- Manfred Schmidt-Schauss (Universität Frankfurt, DE) [dblp]
- Peter H. Schmitt (KIT - Karlsruher Institut für Technologie, DE) [dblp]
- Johann M. Schumann (NASA / RIACS - Moffett Field, US)
- Natarajan Shankar (SRI - Menlo Park, US) [dblp]
- Jörg Siekmann (DFKI - Saarbrücken, DE)
- Terrance Swift (SUNY - Stony Brook, US)
- Andrei Voronkov (University of Manchester, GB) [dblp]
- Uwe Waldmann (MPI für Informatik - Saarbrücken, DE) [dblp]
- Christoph Walther (TU Darmstadt, DE)
- Adnan Yahya (Universität Koblenz-Landau, 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 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 07401: Deduction and Decision Procedures (2007-09-30 - 2007-10-05) (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)
