Integrated Deduction (Dagstuhl Seminar 21371)

Logical reasoning plays a key role in fields as diverse as verification and synthesis, programming language foundations, knowledge engineering, and computer mathematics. Logical reasoning is increasingly important in intelligent systems, such as decision support systems, agent programming environments, and data processing systems, where deduction may provide explanation, course of action, and the capability of learning from missing information. Problem formalization in these domains typically involves multiple mathematical theories, knowledge bases, and ontologies, all of which may be very large. Problem solving requires both efficient automation and sophisticated human-machine interaction. The thrust of this seminar was that the key to unleash the power of computerized logical reasoning is integration, at different abstraction levels. This seminar offered a forum to discuss the issues related to integration of deduction in a diverse range of applications. In terms of reasoning procedures, the presence of both theories and quantifiers in problems from many contexts calls for methodologies to integrate state-of-the-art SMT solvers and automated theorem provers. This leads to investigate techniques such as model-based reasoning and semantic guidance, that were presented and discussed at the seminar. Similarly, the integration of inference rules for higher-order reasoning in inference systems that were born for first-order reasoning, such as superposition, was prominent among the topics debated at the seminar. At the architectural level, the sheer difficulty of the problems calls for the integration of provers and solvers into interactive reasoning environments. These range from higher-order proof assistants with background reasoners as hammers, to interactive program verifiers, both widely covered at the seminar in talks and discussions. The seminar showed how the application of deduction to intelligent systems necessitates the integration of deduction with other paradigms, such as probabilistic reasoning and statistical inferences. In fact, it emerged from the seminar that even systems that are not natively deductive, such as agent programming environments and industrial tools for ontology-based processing, benefit significantly from the integration of deduction. A clear and shared uptake from the seminar was that scalability and usability are crucial challenges at all levels of integration. The seminar fully succeded in promoting the exchange of new ideas and suggestions for future research.