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 erteilen

Jutka Gasiorowski zu administrativen Fragen

Andreas Dolzmann zu wissenschaftlichen Fragen


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.

Motivation text license
  Creative Commons BY 3.0 DE
  Maria Paola Bonacina, Claudia Nalon, 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).


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

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.