https://www.dagstuhl.de/21371
September 12 – 17 , 2021, Dagstuhl Seminar 21371
Integrated Deduction
Organizers
Maria Paola Bonacina (University of Verona, IT)
Claudia Nalon (University of Brasilia, BR)
Philipp Rümmer (Uppsala University, SE)
Renate Schmidt (University of Manchester, GB)
For support, please contact
Jutka Gasiorowski for administrative matters
Andreas Dolzmann for scientific matters
Motivation
The simultaneous growth of automated deduction and of its numerous fields of applications has shown that a wide and diverse range of methods and tools is needed and can be developed. Nowadays such tools exist, including SAT solvers, SMT solvers, automated theorem provers, aka ATP systems, proof assistants, aka interactive theorem provers (ITP), as well as libraries of formalized mathematics and formalized knowledge. Behind each of them there is a substantial body of theoretical work that defines the implemented methods and approaches, proves their properties (e.g., soundness, completeness, termination, complexity), and characterizes formally the problems they can handle.
While essential, logico-deductive reasoning is not the only form of automated reasoning. Intelligent systems, such as decision support systems, agent programming environments, and data processing systems, often employ forms of probabilistic reasoning and statistical inference. Precisely because no method, tool, paradigm, or even reasoning style can solve all problems, or respond to all demands coming from a single field of application, the next grand challenge for automated deduction is integration. Integration occurs and is needed at different abstraction levels, ranging from integration of deductive engines to integration of deduction in intelligent systems, where deduction may provide explanation, course of action, the capability of learning from missing information, aid modelling, and facilitate agent communication. The Dagstuhl Seminar on Integrated Deduction will cover as many as possible of these integration issues:
- Integration of deductive engines into more general automated deductive systems;
- Integration of automated deductive systems into interactive proof assistants;
- Integration of deduction into formal methods tools;
- Integration of deduction for knowledge processing;
- Integration of deduction into intelligent systems such as agent-based systems; and
- Integrated deduction in education.
Furthemore, the seminar will investigate a number of key technological and human-related issues that are largely orthogonal to the above topics, and affect both feasibility and deployment of integrated deduction. Examples of such issues include interface development, extraction of information from intermediate states of automated reasoning systems, reproducibility, collaboration with non-expert users, and use of specialized algorithms.
This Dagstuhl 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 seminar aims at bringing together a diverse audience, including researchers working on deduction, researchers applying deduction, and researchers experienced in integrating deduction. Participants are invited to consider contributing talks on problems that they are working on, but have not solved yet, in order to encourage collaborations.
Motivation text license Creative Commons BY 3.0 DE
Maria Paola Bonacina, Claudia Nalon, Philipp Rümmer, and Renate Schmidt
Dagstuhl Seminar Series
- 19371: "Deduction Beyond Satisfiability" (2019)
- 17371: "Deduction Beyond First-Order Logic" (2017)
- 15381: "Information from Deduction: Models and Proofs" (2015)
- 13411: "Deduction and Arithmetic" (2013)
- 09411: "Interaction versus Automation: The two Faces of Deduction" (2009)
- 07401: "Deduction and Decision Procedures" (2007)
- 05431: "Deduction and Applications" (2005)
- 03171: "Deduction and Infinite-state Model Checking" (2003)
- 01101: "Deduction" (2001)
- 99091: "Deduction" (1999)
- 9709: "Deduction" (1997)
- 9512: "Deduction" (1995)
- 9310: "Deduction" (1993)
Classification
- Artificial Intelligence
- Logic In Computer Science
- Symbolic Computation
Keywords
- Deduction
- Logic
- Automated theorem proving
- Reasoning
- SMT solving