March 4 – 9 , 2001, Dagstuhl Seminar 01101
For support, please 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.
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)
- 07401: "Deduction and Decision Procedures" (2007)
- 05431: "Deduction and Applications" (2005)
- 03171: "Deduction and Infinite-state Model Checking" (2003)
- 99091: "Deduction" (1999)
- 9709: "Deduction" (1997)
- 9512: "Deduction" (1995)
- 9310: "Deduction" (1993)