Dagstuhl-Seminar 26091
Revisiting the Foundations of Deduction in a New World
( 22. Feb – 27. Feb, 2026 )
Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite:
https://www.dagstuhl.de/26091
Organisatoren
- Pascal Fontaine (University of Liège, BE)
- Konstantin Korovin (University of Manchester, GB)
- Martina Seidl (Johannes Kepler Universität Linz, AT)
- Sophie Tourret (INRIA Nancy - Grand Est, FR)
Kontakt
- Marsha Kleinbauer (für wissenschaftliche Fragen)
- Susanne Bach-Bernhard (für administrative Fragen)
Automated deduction is now more than half a century old. Its theoretical foundations, i.e., the notions of soundness, completeness, decidability, and complexity date back to these times or even earlier. In the last couple of decades though, due to the massive development of powerful processors with several to many cores, large, layered, and fast memories, GPUs, machine learning, cloud computing, and huge storage, the world has changed. In this new world, novel infrastructure and techniques often challenge our foundations. For instance, parallel and portfolio solvers question the once revered notion of completeness, in favor of a more vague notion of practical efficiency.
Some time to assess the current status of research on deduction and its future is necessary. Do we need new metrics to evaluate algorithms? What are the positive and negative impacts of benchmarks, and of the industry oriented development of deduction tools? Usually, nobody questions that tools must be sound, but what place is there now for the notions of completeness, decidability, complexity, and proof complexity in modern algorithms? Should we discard them in favor of heuristics, parallelism and machine learning techniques, eagerly following new trends, or should we rather adapt them? How could we adapt them? Is there a divide between attachment to foundational notions and attraction to practical results? If there is, can it be attributed to a generational gap? Is there something our community can and should do to ensure the transmission of important foundational concepts to the younger generation? How can we characterize the theoretical properties of our new algorithms that integrate machine learning, hundreds of strategies and techniques, running in parallel on a large number of computing units in the cloud? Is it possible to reconcile carefully crafted data-structures and algorithms, with massively parallel computing using machine learning techniques?
We need a high vantage point to discuss these changes as a community.
In this Dagstuhl Seminar, we invite the participants to share and to question their assessment of the current status of research on deduction, our metrics of progress and success, and the timeliness of our foundations in this new world.
Creative Commons BY 4.0
Pascal Fontaine, Konstantin Korovin, Martina Seidl, and Sophie Tourret
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 23471: The Next Generation of Deduction Systems: From Composition to Compositionality (2023-11-19 - 2023-11-24) (Details)
Klassifikation
- Artificial Intelligence
- Logic in Computer Science
- Symbolic Computation
Schlagworte
- deduction
- logic
- automated reasoning
- correctness
- complexity
