Integrated Deduction

Summary

This report contains the program and outcomes of the Dagstuhl Seminar 21371 on Integrated Deduction that was held at Schloss Dagstuhl, Leibniz Center for Informatics, during September 12-17, 2017. It was the fourteenth in a series of Dagstuhl Deduction seminars held biennially since 1993.

The motivation for this seminar was the following. Automated deduction has developed a wide and diverse range of methods and tools for logico-deductive reasoning. They include 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. These methods and tools have found successful application in computing fields as diverse as the analysis, verification, and synthesis of systems, programming language design, knowledge engineering, and computer mathematics. However, no method, tool, paradigm, or even reasoning style can solve all problems, or respond to all demands coming from even a single field of application. Therefore, the next grand challenge for automated deduction is integration.

Integration occurs and is needed at different abstraction levels. Within deduction itself, integration of deductive engines allows us to build more powerful, more flexible, more expressive reasoners, that can solve more problems with fewer resources, meaning not only memory and computing time, but also human time and human expertise, the latter two often being the most precious of resources. Next, deductive reasoners get integrated into other tools, such as automated test generators, verifying compilers, or program synthesizers, just to name a few. Yet another level of integration occurs when logico-deductive reasoning is integrated with other forms of automated reasoning, such as probabilistic reasoning and statistical inference. This leads to the integration of deduction within intelligent systems, such as decision support systems, agent programming environments, and data processing systems. Here deduction may provide explanation, course of action, and the capability of learning from missing information; it may also aid modelling and facilitate agent communication.

The seminar on Integrated Deduction successfully covered as many as possible of these integration issues, including:

• 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; and
• Integration of deduction into intelligent systems such as agent-based systems.

Furthemore, the seminar investigated a number of key technological and human-related issues, that are largely orthogonal to most integration contexts, affecting both feasibility and deployment of integrated deduction. Examples of such issues are:

• The development of interfaces for integration;
• The generation of continuous feedback during the run of deductive tools, including also information from intermediate or unsuccessful states;
• The reproducibility of results in the presence of tool updates or imposed resource limits (e.g., available computation time or memory) that may introduce non-determinism; and
• Advanced tradeoff's between performance and expressivity as well as between specialization and genericity.

Practical challenges around integrated deductive systems, including collaboration with non-expert users or access to data sets, were also discussed.

The seminar brought together a diverse audience, including both researchers working in deduction and researchers working in neighbouring areas that make use of deduction. Many participants have experience in building, using, and applying systems with integrated deduction.

Following the tradition of the Dagstuhl Seminars on Deduction, most of the program consisted of contributed talks by participants on their research. In this manner, the bottom-up style of the Dagstuhl experience was preserved, allowing for spontaneous contributions as they emerged during the seminar.

However, this seminar was also innovative with respect to tradition, in that it featured five invited tutorials on key topics in integrated deduction. These tutorials were valuable in highlighting the state-of-the-art in the integration of deduction systems and in fomenting discussions on challenges and open problems.

The program also featured a hike in the woods and a social dinner in a nearby village, that helped establishing or strengthtening collaborations.

The following section contains the abstracts for most of the talks and tutorials listed in alphabetical order.