TOP
Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 21371

Integrated Deduction

( Sep 12 – Sep 17, 2021 )

(Click in the middle of the image to enlarge)

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/21371

Organizers

Contact


Schedule

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.

Copyright Maria Paola Bonacina, Claudia Nalon, Philipp Rümmer, and Renate Schmidt

Summary

This report contains the program and outcomes of the Dagstuhl Seminar 21371 on Integrated Deduction that was held at Schloss Dagstuhl, Leibniz Center for Informatics, during September 12-17, 2017. It was the fourteenth in a series of Dagstuhl Deduction seminars held biennially since 1993.

The motivation for this seminar was the following. Automated deduction has developed a wide and diverse range of methods and tools for logico-deductive reasoning. They include 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. These methods and tools have found successful application in computing fields as diverse as the analysis, verification, and synthesis of systems, programming language design, knowledge engineering, and computer mathematics. However, no method, tool, paradigm, or even reasoning style can solve all problems, or respond to all demands coming from even a single field of application. Therefore, the next grand challenge for automated deduction is integration.

Integration occurs and is needed at different abstraction levels. Within deduction itself, integration of deductive engines allows us to build more powerful, more flexible, more expressive reasoners, that can solve more problems with fewer resources, meaning not only memory and computing time, but also human time and human expertise, the latter two often being the most precious of resources. Next, deductive reasoners get integrated into other tools, such as automated test generators, verifying compilers, or program synthesizers, just to name a few. Yet another level of integration occurs when logico-deductive reasoning is integrated with other forms of automated reasoning, such as probabilistic reasoning and statistical inference. This leads to the integration of deduction within intelligent systems, such as decision support systems, agent programming environments, and data processing systems. Here deduction may provide explanation, course of action, and the capability of learning from missing information; it may also aid modelling and facilitate agent communication.

The seminar on Integrated Deduction successfully covered as many as possible of these integration issues, including:

  • 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; and
  • Integration of deduction into intelligent systems such as agent-based systems.

Furthemore, the seminar investigated a number of key technological and human-related issues, that are largely orthogonal to most integration contexts, affecting both feasibility and deployment of integrated deduction. Examples of such issues are:

  • The development of interfaces for integration;
  • The generation of continuous feedback during the run of deductive tools, including also information from intermediate or unsuccessful states;
  • The reproducibility of results in the presence of tool updates or imposed resource limits (e.g., available computation time or memory) that may introduce non-determinism; and
  • Advanced tradeoff's between performance and expressivity as well as between specialization and genericity.

Practical challenges around integrated deductive systems, including collaboration with non-expert users or access to data sets, were also discussed.

The seminar brought together a diverse audience, including both researchers working in deduction and researchers working in neighbouring areas that make use of deduction. Many participants have experience in building, using, and applying systems with integrated deduction.

Following the tradition of the Dagstuhl Seminars on Deduction, most of the program consisted of contributed talks by participants on their research. In this manner, the bottom-up style of the Dagstuhl experience was preserved, allowing for spontaneous contributions as they emerged during the seminar.

However, this seminar was also innovative with respect to tradition, in that it featured five invited tutorials on key topics in integrated deduction. These tutorials were valuable in highlighting the state-of-the-art in the integration of deduction systems and in fomenting discussions on challenges and open problems.

The program also featured a hike in the woods and a social dinner in a nearby village, that helped establishing or strengthtening collaborations.

The following section contains the abstracts for most of the talks and tutorials listed in alphabetical order.

Copyright Maria Paola Bonacina, Philipp Rümmer, and Renate Schmidt

Participants
  • Erika Abraham (RWTH Aachen University, DE) [dblp]
  • Alexander Bentkamp (VU University Amsterdam, NL) [dblp]
  • Jasmin Christian Blanchette (VU University Amsterdam, NL) [dblp]
  • Maria Paola Bonacina (University of Verona, IT) [dblp]
  • Pascal Fontaine (University of Liège, BE) [dblp]
  • Carsten Fuhs (Birkbeck, University of London, GB) [dblp]
  • Stéphane Graham-Lengrand (SRI - Menlo Park, US) [dblp]
  • Ullrich Hustadt (University of Liverpool, GB) [dblp]
  • Moa Johansson (Chalmers University of Technology - Göteborg, SE) [dblp]
  • Patrick Koopmann (TU Dresden, DE) [dblp]
  • Magnus Myreen (Chalmers University of Technology - Göteborg, SE) [dblp]
  • Ruzica Piskac (Yale University - New Haven, US) [dblp]
  • Philipp Rümmer (Uppsala University, SE) [dblp]
  • Renate Schmidt (University of Manchester, GB) [dblp]
  • Claudia Schon (Universität Koblenz-Landau, DE) [dblp]
  • Stephan Schulz (Duale Hochschule Baden-Württemberg - Stuttgart, DE) [dblp]
  • Alexander Steen (University of Luxembourg, LU) [dblp]
  • Martin Suda (Czech Technical University - Prague, CZ) [dblp]
  • Sophie Tourret (INRIA Nancy - Grand Est - Villers-lès-Nancy, FR & MPI für Informatik - Saarbrücken, DE) [dblp]
  • Sarah Winkler (University of Verona, IT) [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 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 theorem proving
  • reasoning
  • SMT solving