Dagstuhl-Seminar 23471
The Next Generation of Deduction Systems: from Composition to Compositionality
( 19. Nov – 24. Nov, 2023 )
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 Brasilia, BR)
- Claudia Schon (Hochschule Trier, DE)
Kontakt
- Andreas Dolzmann (für wissenschaftliche Fragen)
- Susanne Bach-Bernhard (für administrative Fragen)
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
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)
Klassifikation
- Artificial Intelligence
- Logic in Computer Science
- Symbolic Computation
Schlagworte
- deduction
- logic
- automated reasoning
- compositionality
- artificial intelligence
