Integrated Deduction (Dagstuhl Seminar 21371)

Authors Maria Paola Bonacina, Philipp Rümmer, Renate A. Schmidt and all authors of the abstracts in this report

Thumbnail PDF


  • Filesize: 2.93 MB
  • 17 pages

Document Identifiers

Author Details

Maria Paola Bonacina
  • Università degli Studi di Verona, IT
Philipp Rümmer
  • Uppsala University, SE
Renate A. Schmidt
  • University of Manchester, GB
and all authors of the abstracts in this report

Cite AsGet BibTex

Maria Paola Bonacina, Philipp Rümmer, and Renate A. Schmidt. Integrated Deduction (Dagstuhl Seminar 21371). In Dagstuhl Reports, Volume 11, Issue 8, pp. 35-51, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Logical reasoning plays a key role in fields as diverse as verification and synthesis, programming language foundations, knowledge engineering, and computer mathematics. Logical reasoning is increasingly important in intelligent systems, such as decision support systems, agent programming environments, and data processing systems, where deduction may provide explanation, course of action, and the capability of learning from missing information. Problem formalization in these domains typically involves multiple mathematical theories, knowledge bases, and ontologies, all of which may be very large. Problem solving requires both efficient automation and sophisticated human-machine interaction. The thrust of this seminar was that the key to unleash the power of computerized logical reasoning is integration, at different abstraction levels. This seminar offered a forum to discuss the issues related to integration of deduction in a diverse range of applications. In terms of reasoning procedures, the presence of both theories and quantifiers in problems from many contexts calls for methodologies to integrate state-of-the-art SMT solvers and automated theorem provers. This leads to investigate techniques such as model-based reasoning and semantic guidance, that were presented and discussed at the seminar. Similarly, the integration of inference rules for higher-order reasoning in inference systems that were born for first-order reasoning, such as superposition, was prominent among the topics debated at the seminar. At the architectural level, the sheer difficulty of the problems calls for the integration of provers and solvers into interactive reasoning environments. These range from higher-order proof assistants with background reasoners as hammers, to interactive program verifiers, both widely covered at the seminar in talks and discussions. The seminar showed how the application of deduction to intelligent systems necessitates the integration of deduction with other paradigms, such as probabilistic reasoning and statistical inferences. In fact, it emerged from the seminar that even systems that are not natively deductive, such as agent programming environments and industrial tools for ontology-based processing, benefit significantly from the integration of deduction. A clear and shared uptake from the seminar was that scalability and usability are crucial challenges at all levels of integration. The seminar fully succeded in promoting the exchange of new ideas and suggestions for future research.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
  • Automated theorem proving
  • deduction
  • logic
  • reasoning
  • SMT solving


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads