September 12 – 17 , 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)

For support, please contact

Jutka Gasiorowski for administrative matters

Andreas Dolzmann for scientific matters


List of Participants
Shared Documents
Dagstuhl Seminar Schedule [pdf]


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 the series Dagstuhl Reports each Dagstuhl Seminar and Dagstuhl Perspectives Workshop is documented. The seminar organizers, in cooperation with the collector, prepare a report that includes contributions from the participants' talks together with a summary of the seminar.


Download overview leaflet (PDF).


Furthermore, a comprehensive peer-reviewed collection of research papers can be published in the series Dagstuhl Follow-Ups.

Dagstuhl's Impact

Please inform us when a publication was published as a result from your seminar. These publications are listed in the category Dagstuhl's Impact and are presented on a special shelf on the ground floor of the library.