12. – 17. September 2021, Dagstuhl-Seminar 21371

Integrated Deduction


Maria Paola Bonacina (University of Verona, IT)
Claudia Nalon (University of Brasilia, BR)
Philipp Rümmer (Uppsala University, SE)
Renate Schmidt (University of Manchester, GB)

Auskunft zu diesem Dagstuhl-Seminar erteilt

Dagstuhl Service Team


Dagstuhl Report, Volume 11, Issue 8 Dagstuhl Report
Gemeinsame Dokumente
Programm des Dagstuhl-Seminars [pdf]


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.

Summary text license
  Creative Commons BY 4.0
  Maria Paola Bonacina, Philipp Rümmer, and Renate Schmidt

Dagstuhl-Seminar Series


  • Artificial Intelligence
  • Logic In Computer Science
  • Symbolic Computation


  • Deduction
  • Logic
  • Automated theorem proving
  • Reasoning
  • SMT solving


In der Reihe Dagstuhl Reports werden alle Dagstuhl-Seminare und Dagstuhl-Perspektiven-Workshops dokumentiert. Die Organisatoren stellen zusammen mit dem Collector des Seminars einen Bericht zusammen, der die Beiträge der Autoren zusammenfasst und um eine Zusammenfassung ergänzt.


Download Übersichtsflyer (PDF).

Dagstuhl's Impact

Bitte informieren Sie uns, wenn eine Veröffentlichung ausgehend von Ihrem Seminar entsteht. Derartige Veröffentlichungen werden von uns in der Rubrik Dagstuhl's Impact separat aufgelistet  und im Erdgeschoss der Bibliothek präsentiert.


Es besteht weiterhin die Möglichkeit, eine umfassende Kollektion begutachteter Arbeiten in der Reihe Dagstuhl Follow-Ups zu publizieren.