November 19 – 24 , 2023, Dagstuhl Seminar 23471

The Next Generation of Deduction Systems: from Composition to Compositionality


Maria Paola Bonacina (University of Verona, IT)
Pascal Fontaine (University of Liège, BE)
Claudia Nalon (University of Brasilia, BR)
Claudia Schon (Universität Koblenz-Landau, DE)

For support, please contact

Susanne Bach-Bernhard for administrative matters

Andreas Dolzmann for scientific matters


Automated deduction is now more than half a century old (e.g., 2023 is the 60th anniversary of the resolution principle), and has reached a certain level of maturity. Thanks to the generality of logical reasoning and the expressive power of many available logics, tools for automated deduction are applied successfully in fields ranging from artificial intelligence to programming languages, verification, synthesis, program analysis, and scheduling. However, new challenges for the field of automated deduction emerge:

  • Many real-world problems require increasingly complex, large, and heterogeneous logics, formulas, theories, and knowledge bases. The size and diversity of proofs and models increase accordingly.
  • Satisfiability and validity remain fundamentally difficult computational problems and reasoners may run out of time or memory, or demand too much human labor.
  • The vast array of techniques available in deduction is often implemented only as short-lived prototypes whose transfer to stable systems is uncertain. Over time systems may become too big, monolithic, and unwieldy for further development. Portfolios of techniques may be useful for experiments, but do not seem to facilitate a conceptual synthesis or a breakthrough. The field faces a "software crisis" that is also a "techniques crisis".

Approaches based on composition will be especially important to meet these challenges. A composition is a combination of components such that properties of the components are preserved (e.g., soundness, completeness, termination, model-construction). The Dagstuhl Seminar on The Next Generation of Deduction Systems: from Composition to Compositionality aims at addressing these challenges by discussing the following topics:

  • Composition of rule systems and composition of strategies;
  • Composition of reasoning and learning;
  • Composition of proofs, theories, and models;
  • Composition of reasoning systems and knowledge systems; and
  • The engineering of compositional deduction systems, where compositionality is the concrete software property that is expected to correspond to composition at the abstract level.

The 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 aim is to offer participants not only a forum to present their research and receive feed-back, but also opportunities to discover their next research quest or collaboration.

The seminar aims to bring together a diverse audience including researchers working in deduction and experts in building and applying reasoning systems and knowledge systems. Participants are invited to consider contributing talks on problems that they are working on, but have not solved yet, in order to foster discussions and encourage collaborations.

Motivation text license
  Creative Commons BY 4.0
  Maria Paola Bonacina, Pascal Fontaine, Claudia Nalon, and Claudia Schon

Dagstuhl Seminar Series


  • Artificial Intelligence
  • Logic In Computer Science
  • Symbolic Computation


  • Deduction
  • Logic
  • Automated reasoning
  • Compositionality
  • Artificial intelligence


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).

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.


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