Dagstuhl-Seminar 23471
The Next Generation of Deduction Systems: From Composition to Compositionality
( 19. Nov – 24. Nov, 2023 )
(zum Vergrößern in der Bildmitte klicken)
Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:
https://www.dagstuhl.de/23471
Organisatoren
- Maria Paola Bonacina (University of Verona, IT)
- Pascal Fontaine (University of Liège, BE)
- Claudia Nalon (University of Brasília, BR)
- Claudia Schon (Hochschule Trier, DE)
Kontakt
- Andreas Dolzmann (für wissenschaftliche Fragen)
- Susanne Bach-Bernhard (für administrative Fragen)
Programm
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:
- 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.
- 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.
- 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.
Creative Commons BY 4.0
Maria Paola Bonacina, Pascal Fontaine, Claudia Nalon, and Claudia Schon
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.
Maria Paola Bonacina, Pascal Fontaine, Claudia Nalon, and Claudia Schon
- Franz Baader (TU Dresden, DE) [dblp]
- Haniel Barbosa (Federal University of Minas Gerais-Belo Horizonte, BR) [dblp]
- Maria Paola Bonacina (University of Verona, IT) [dblp]
- David Déharbe (CLEARSY - Aix-en-Provence, FR) [dblp]
- Martin Desharnais (Max-Planck-Institut für Informatik Saarbrücken, DE) [dblp]
- Clare Dixon (University of Manchester, GB) [dblp]
- Catherine Dubois (ENSIIE - Evry, FR) [dblp]
- Amy Felty (University of Ottawa, CA) [dblp]
- Pascal Fontaine (University of Liège, BE) [dblp]
- Silvio Ghilardi (University of Milan, IT) [dblp]
- Antti Hyvärinen (Certora - Pregassona, CH)
- Fuqi Jia (Chinese Academy of Sciences, CN) [dblp]
- Chantal Keller (ENS - Gif-sur-Yvette, FR) [dblp]
- Cynthia Kop (Radboud University Nijmegen, NL) [dblp]
- Konstantin Korovin (University of Manchester, GB) [dblp]
- Hanna Lachnitt (Stanford University, US) [dblp]
- Feifei Ma (Chinese Academy of Sciences - Beijing, CN) [dblp]
- Jasper Nalbach (RWTH Aachen, DE) [dblp]
- Claudia Nalon (University of Brasília, BR) [dblp]
- Jakob Nordström (University of Copenhagen, DK & Lund University, SE) [dblp]
- Florian Rabe (Universität Erlangen-Nürnberg, DE) [dblp]
- Andrew Reynolds (University of Iowa - Iowa City, US) [dblp]
- Claudia Schon (Hochschule Trier, DE) [dblp]
- Stephan Schulz (Duale Hochschule Baden-Württemberg - Stuttgart, DE) [dblp]
- Martina Seidl (Johannes Kepler Universität Linz, AT) [dblp]
- Nick Smallbone (Chalmers University of Technology - Göteborg, SE) [dblp]
- Viorica Sofronie-Stokkermans (Universität Koblenz, DE) [dblp]
- Alexander Steen (Universität Greifswald, DE) [dblp]
- Geoff Sutcliffe (University of Miami, US) [dblp]
- Sophie Tourret (INRIA Nancy - Grand Est, FR) [dblp]
- Uwe Waldmann (MPI für Informatik - Saarbrücken, DE) [dblp]
- Christoph Weidenbach (MPI für Informatik - Saarbrücken, DE) [dblp]
- Akihisa Yamada (AIST - Tokyo, JP) [dblp]
Verwandte Seminare
- 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)
- Dagstuhl-Seminar 26091: Revisiting the Foundations of Deduction in a New World (2026-02-22 - 2026-02-27) (Details)
Klassifikation
- Artificial Intelligence
- Logic in Computer Science
- Symbolic Computation
Schlagworte
- deduction
- logic
- automated reasoning
- compositionality
- artificial intelligence
