Dagstuhl Seminar 26091
Revisiting the Foundations of Deduction in a New World
( Feb 22 – Feb 27, 2026 )
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/26091
Organizers
- 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)
Contact
- Marsha Kleinbauer (for scientific matters)
- Susanne Bach-Bernhard (for administrative matters)
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
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)
- Dagstuhl Seminar 23471: The Next Generation of Deduction Systems: From Composition to Compositionality (2023-11-19 - 2023-11-24) (Details)
Classification
- Artificial Intelligence
- Logic in Computer Science
- Symbolic Computation
Keywords
- deduction
- logic
- automated reasoning
- correctness
- complexity
