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
- 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)
Contact
- Andreas Dolzmann (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
Dagstuhl Reports
As part of the mandatory documentation, participants are asked to submit their talk abstracts, working group results, etc. for publication in our series Dagstuhl Reports via the Dagstuhl Reports Submission System.
- Upload (Use personal credentials as created in DOOR to log in)
Dagstuhl Seminar Wiki
- Dagstuhl Seminar Wiki (Use personal credentials as created in DOOR to log in)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
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
- 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 Joseph 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]
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
