Integrated Deduction

Motivation

The simultaneous growth of automated deduction and of its numerous fields of applications has shown that a wide and diverse range of methods and tools is needed and can be developed. Nowadays such tools exist, including SAT solvers, SMT solvers, automated theorem provers, aka ATP systems, proof assistants, aka interactive theorem provers (ITP), as well as libraries of formalized mathematics and formalized knowledge. Behind each of them there is a substantial body of theoretical work that defines the implemented methods and approaches, proves their properties (e.g., soundness, completeness, termination, complexity), and characterizes formally the problems they can handle.

While essential, logico-deductive reasoning is not the only form of automated reasoning. Intelligent systems, such as decision support systems, agent programming environments, and data processing systems, often employ forms of probabilistic reasoning and statistical inference. Precisely because no method, tool, paradigm, or even reasoning style can solve all problems, or respond to all demands coming from a single field of application, the next grand challenge for automated deduction is integration. Integration occurs and is needed at different abstraction levels, ranging from integration of deductive engines to integration of deduction in intelligent systems, where deduction may provide explanation, course of action, the capability of learning from missing information, aid modelling, and facilitate agent communication. The Dagstuhl Seminar on Integrated Deduction will cover as many as possible of these integration issues:

• Integration of deductive engines into more general automated deductive systems;
• Integration of automated deductive systems into interactive proof assistants;
• Integration of deduction into formal methods tools;
• Integration of deduction for knowledge processing;
• Integration of deduction into intelligent systems such as agent-based systems; and
• Integrated deduction in education.

Furthemore, the seminar will investigate a number of key technological and human-related issues that are largely orthogonal to the above topics, and affect both feasibility and deployment of integrated deduction. Examples of such issues include interface development, extraction of information from intermediate states of automated reasoning systems, reproducibility, collaboration with non-expert users, and use of specialized algorithms.

This Dagstuhl Seminar will be organized as a combination of contributed talks, invited tutorials, and discussion sessions. Discussion sessions will go beyond the standard question time at the end of talks, with both plenary and breakout discussion sessions interleaved with the technical sessions made of talks or tutorials.

The seminar aims at bringing together a diverse audience, including researchers working on deduction, researchers applying deduction, and researchers experienced in integrating deduction. Participants are invited to consider contributing talks on problems that they are working on, but have not solved yet, in order to encourage collaborations.