TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Please select your role
to obtain appropriate quick-links.
As a LIPIcs/OASIcs author, you will be invited by e-mail to register at the Dagstuhl Submission Server. The server will guide you through the publication workflow. Preliminary information can be found here:
Quick Links

Dagstuhl Seminar 23471

The Next Generation of Deduction Systems: From Composition to Compositionality

( Nov 19 – Nov 24, 2023 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/23471
Organizers
Contact
Shared Documents
Publications
Schedule
Summary
Show Summary

The full report contains the program and outcomes of the Dagstuhl Seminar 23471 on The Next Generation of Deduction Systems: From Composition to Compositionality that was held at Schloss Dagstuhl, Leibniz Center for Informatics, during November 19--24, 2023. It was the fifteenth in a series of Dagstuhl Deduction seminars held biennially since 1993.

The motivation for this seminar was threefold:

  1. Automated reasoning tools, including SAT solvers, SMT solvers, theorem provers, and proof assistants, are widely applied in fields as diverse as analysis/verification/synthesis of systems, programming language design, knowledge engineering, computer mathematics, natural language processing, and robotics. However, satisfiability and validity remain fundamentally difficult computational problems, so that reasoners may run out of time or memory returning ``don't know'' or may demand too much human labor.
  2. After the low-hanging fruits have been picked, the formalization of problems require logics, formulas, theories, and knowledge bases that are increasingly complex, large, and heterogeneous. The size and diversity of the proofs and models, that reasoners produce to support their answers, increase accordingly.
  3. Deduction offers a vast array of techniques, but many implementations of new techniques remain short-lived prototypes, and the transfer of the successful ones into more stable systems is uncertain. Relatively few systems gather most of the resources, but over time they may become too big, monolithic, and unwieldy for further development, or resort to assemble techniques into portfolios. A portfolio allows one to experiment and may win competitions, but it hardly leads to a conceptual synthesis and hence a breakthrough.

The Dagstuhl Seminar on The Next Generation of Deduction Systems: From Composition to Compositionality addressed these issues by challenging participants to reflect around the ideas of composition and compositionality.

A composition is a combination such that properties of the components (e.g., soundness, completeness, termination, model-construction) are preserved. Since different inference systems have different strengths, their composition is essential to meet Challenge (1). For example, the seminar participants presented and discussed research about the composition of equality reasoning by superposition with instance-based (e.g., Inst-gen - "Instance Generation") or model-based (e.g., SCL - "Simple Clause Learning") inference systems.

A major cause of "don't know" answers in satisfiability modulo theories (SMT) is the fact that most decision procedures inside SMT solvers are for quantifier-free fragments of theories, whereas applications require handling quantified formulas. Thus, the seminar addressed the fundamental problem of composing quantifier reasoning and theory reasoning. For example, the QSMA algorithm, where QSMA stands for "Quantified Satisfiability Modulo Assignment," offers a novel solution for quantifier reasoning in a complete theory (e.g., arithmetic).

Historically, proof generation was deemed unproblematic in automated theorem provers, whereas model generation was deemed unproblematic in SMT solving. This is why recent research has focused on proofs in SMT and models in first-order theorem proving. The seminar reflected these trends. Several talks presented advanced research on proof production in SMT, involving composition of proofs, both within the SMT solver, as in composition of proofs from different theories, and at the interface of the SMT solver (e.g., CVC5) with a proof assistant (e.g., Lean, Isabelle/HOL). At the next abstraction level, the seminar analyzed these issues in logical frameworks (e.g., Hybrid, Dedukti), where proofs from different proof assistants may be verified, exchanged, translated, and hence re-verified. Work on the representation and composition of first-order models in libraries of problems for first-order theorem provers (e.g., TPTP) is also gaining momentum, and the seminar offered an excellent discussion forum, since several developers of theorem provers were attending.

The drive to improve the search capabilities of deduction procedures in order to meet Challenge (1) leads also to the composition of reasoning and learning, while Challenge (2) leads to the composition of reasoning systems and knowledge systems. Learning is a native capability of automated reasoners, as in lemma learning. SAT/SMT solvers and theorem provers learn within a derivation by learning lemmas to reduce the search space by avoiding repeated work. Reasoners also learn across derivations by applying machine learning to learn from a very high number of derivations which strategies or tactics to select for an input problem with certain features. The composition of reasoning and learning was discussed at the seminar in SAT solving, and in resolution-based first-order theorem proving, where the prover is interfaced with an ontology-based knowledge system (e.g., Adimen SUMO).

The sentiment that emerged at the seminar is that approaches based on composition will contribute to meet Challenge (3), by endowing deduction systems with compositionality, towards going beyond portfolios. The participants discussed the crisis of growth that the field is facing, given the rise of so many rule systems, strategies, and techniques. Since it is a crisis of growth, the field will emerge from it even stronger. For this to happen, however, it is key to address the issues that make it difficult to transfer new ideas into stable and useable deduction systems. The existing dichotomy, between short-lived prototypes and powerful, but big, monolithic, unwieldy systems, was discussed as an automated reasoning software crisis. The need for modularity was recognized, and a distinction between industry powertools and pedagogical platforms was outlined. The latter will have to give up on a unique programming language and programming style, as well as on award-winning efficiency, but will facilitate the entrance of new students, currently discouraged by the impossibility of competing with established tools. Thanks to such platforms, the building of new systems will be less expensive in terms of human time and labor. The risk of new ideas being forgotten without having been properly implemented and tested will be reduced.

The atmosphere throughout the seminar was excellent. For example, a participant told one of the organizers that this seminar motivated them and rekindled their enthusiasm for automated deduction research. An outing - an excursion to Bernkastel-Kues followed by a social dinner in a nearby village - also contributed to establishing a relaxed, friendly atmosphere, conducive to new or strengthtened collaborations.

The bottom-up style of the Dagstuhl experience was preserved, thanks to a flexible program that allowed the participants to volunteer topics and talks throughout the gathering. This seminar maintained a feature that was introduced in the 2021 edition, namely the possibility of giving a tutorial using two time slots rather than one. Altogether, five tutorials were given on topics ranging from proofs in SMT, reasoning with quantifiers in SMT, composition of reasoning and neuro-symbolic methods, and model-based reasoning.

The full report contains the abstracts for most of the talks and tutorials listed in alphabetical order.

Copyright Maria Paola Bonacina, Pascal Fontaine, Claudia Nalon, and Claudia Schon
Motivation
Show Motivation

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.

Copyright Maria Paola Bonacina, Pascal Fontaine, Claudia Nalon, and Claudia Schon
Participants
Show Participants
Related Seminars
  • Dagstuhl Seminar 9310: Deduction (1993-03-08 - 1993-03-12) (Details)
  • Dagstuhl Seminar 9512: Deduction (1995-03-20 - 1995-03-24) (Details)
  • Dagstuhl Seminar 9709: Deduction (1997-02-24 - 1997-02-28) (Details)
  • Dagstuhl Seminar 99091: Deduction (1999-02-28 - 1999-03-05) (Details)
  • Dagstuhl Seminar 01101: Deduction (2001-03-04 - 2001-03-09) (Details)
  • Dagstuhl Seminar 03171: Deduction and Infinite-state Model Checking (2003-04-21 - 2003-04-25) (Details)
  • Dagstuhl Seminar 05431: Deduction and Applications (2005-10-23 - 2005-10-28) (Details)
  • Dagstuhl Seminar 07401: Deduction and Decision Procedures (2007-09-30 - 2007-10-05) (Details)
  • Dagstuhl Seminar 09411: Interaction versus Automation: The two Faces of Deduction (2009-10-04 - 2009-10-09) (Details)
  • Dagstuhl Seminar 13411: Deduction and Arithmetic (2013-10-06 - 2013-10-11) (Details)
  • Dagstuhl Seminar 15381: Information from Deduction: Models and Proofs (2015-09-13 - 2015-09-18) (Details)
  • Dagstuhl Seminar 17371: Deduction Beyond First-Order Logic (2017-09-10 - 2017-09-15) (Details)
  • Dagstuhl Seminar 19371: Deduction Beyond Satisfiability (2019-09-08 - 2019-09-13) (Details)
  • Dagstuhl Seminar 21371: Integrated Deduction (2021-09-12 - 2021-09-17) (Details)
Classification
  • Artificial Intelligence
  • Logic in Computer Science
  • Symbolic Computation
Keywords
  • deduction
  • logic
  • automated reasoning
  • compositionality
  • artificial intelligence
Seminar 23471
© 2024 Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH
ImprintContactAccessibilityPrivacy