Search Results

Deduction systems are computer procedures that employ inference or transition rules, search strategies, and multiple supporting algorithms, to solve problems by logico-deductive reasoning. They are at the heart of SAT/SMT solvers, theorem provers, and proof assistants. The wide range of successful applications of these tools shows how logico-deductive reasoning is well-suited for machines. Nonetheless, satisfiability and validity are difficult problems, and applications require reasoners to handle large and heterogeneous knowledge bases, and to generate proofs and models of increasing size and diversity. Thus, a vast array of techniques was developed, leading to what was identified during the seminar as a crisis of growth. This crisis manifests itself also as a software crisis, called automated reasoning software crisis at the seminar. Many deduction systems remain prototypes, while relatively few established systems resort to assemble techniques into portfolios that are useful for experiments, but do not lead to breakthroughs. In order to address this crisis of growth, the Dagstuh Seminar "The Next Generation of Deduction Systems: From Composition to Compositionality" (23471) focused on the key concept of composition, that is, a combination where properties of the components are preserved. Composition applies to all building blocks of deduction: rule systems, strategies, proofs, and models. All these instances of compositions were discussed during the seminar, including for example composition of instance-based and superposition-based inference systems, and composition of modules towards proof production in SMT solvers. Other kinds of composition analyzed during the seminar include the composition of reasoning and learning, and the composition of reasoning systems and knowledge systems. Indeed, reasoners learn within and across derivations, while for applications, from verification to robotics, provers and solvers need to work with other knowledge-based components. In order to address the automated reasoning software crisis, the seminar elaborated the concept of compositionality, as the engineering counterpart of what is composition at the theory and design levels. The seminar clearly identified modularity as the first step towards compositionality, proposing to decompose existing systems into libraries of modules that can be recomposed in new systems. The ensuing discussion led to the distinction between automated reasoners that are industry powertools and automated reasoners that are pedagogical tools. At the societal level, this distinction is important to counter the phenomenon whereby new students are either discouraged by the impossibility of competing with industry powertools, or induced to join only those research groups that work on industry powertools. In summary, the seminar fully succeeded in promoting the exchange of ideas and suggestions for future work.

The seminar focused on satisfiability checking for combinations of first-order logic and subclasses thereof with arithmetic theories in a very liberal sense, also covering quantifiers and parameters. It gathered members of the two communities of symbolic computation (or computer algebra) and satisfiability checking (including satisfiability modulo theories). Up-to-now, these two communities have been working quite independently. We are confident that the seminar will initiate cross-fertilization of both fields and bring improvements for both satisfiability checking and symbolic computation, and for their applications.