Interaction versus Automation: The two Faces of Deduction

Press Review

• Interaktion versus Automatisierung: Die zwei Gesichter der Deduktion.
  Wolfgang Back und Wolfgang Rudolph vom Computerclub Zwei im Gespräch mit Prof. Dr. Jürgen Giesl (Interiew ab 10:15 min)

Motivation

Throughout the history of modern logic, there have been two strands of research: finding natural inference systems for a given problem domain and finding automatic procedures for solving specific logical problems. In computer science, these two strands became interactive and automated deduction.

However, none of the two kinds of systems were ideal for program verification. The interactive tools lacked the necessary automation and the automatic tools failed to cater for important aspects like arithmetic. And neither scaled well. Therefore a separate third, application-driven set of techniques and tools were developed. These are based on powerful automatic procedures for particular logical theories, ranging from propositional logic to arithmetic, and their combination, most notably in the form of SMT solvers. At the same time they were integrated with techniques from program analysis and automata theory. Again, a separate scientific community evolved.

Goals

The seminar is the seventh in the series of Dagstuhl Seminars on "Deduction" (held biennially since 1993).It will bring together the best researchers working on interactive and automatic deduction methods and tools, with a special emphasis on applications to program analysis and verification. The aim is to exploit synergies among the three different approaches discussed above. In particular, combinations of techniques and tools from the different approaches often raise questions and problems that require more interaction between the communities involved.