Dagstuhl Seminar 23471
The Next Generation of Deduction Systems: from Composition to Compositionality
( Nov 19 – Nov 24, 2023 )
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/23471
Organizers
- Maria Paola Bonacina (University of Verona, IT)
- Pascal Fontaine (University of Liège, BE)
- Claudia Nalon (University of Brasilia, BR)
- Claudia Schon (Hochschule Trier, DE)
Contact
- Andreas Dolzmann (for scientific matters)
- Susanne Bach-Bernhard (for administrative 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.
Creative Commons BY 4.0
Maria Paola Bonacina, Pascal Fontaine, Claudia Nalon, and Claudia Schon
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
