Deduction and Applications

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, be it fully automatic, or in interaction with humans. Some progress, however, has been made in the past ten years:

• Automated theorem provers and finite model building programs solved various open mathematical problems of combinatorial nature.
• Model checking, a form of theorem proving over finite models, has become a very successful push-button method for verifying nontrivial safety properties of hardware and software.
• Automated deduction, in particular for so-called 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 together with previous Dagstuhl seminars on "Deduction" have been instrumental in obtaining these successes.

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 as a means to fight fragmentation has lead to successful new conferences like FLoC and IJCAR, and to IFCoLoG, the recently established International Federation for Computational Logic.

This interdisciplinary view of logic in computer science motivated the Dagstuhl seminar. Specifically, we considered several application areas:

• Software verification
• Hardware verification
• Cryptographic protocols
• Programming languages
• Formal methods
• Semantic Web
• Large knowledge bases.