Instantiation- and Learning-Based Methods in Equational Reasoning

In the last 15 years a substantial amount of research has been dedicated to the Boolean satisfiability problem (SAT). As an NP-complete problem it has long been considered intractable. Thus the performance boost exhibited by SAT solvers in the last decade has been astonishing, as by now SAT solvers are mature enough to be used in a wide range of applications, for instance planning tasks and automatic hardware verification. The success of SAT in practice is also reflected in the field of automated reasoning: (1) Instantiation-based theorem proving approaches are used for first-order reasoning, for instance the InstGen framework underlying the theorem prover iProver. In the annual CADE System Competition, iProver beats traditional tools in several important divisions. (2) Maximal completion constitutes a SAT-based approach specifically tailored to equational reasoning, which also turned out to improve over non-SAT-based tools both power- and performance-wise. In this project we want to push the frontiers of SAT in theorem proving even further. In the first place, we will combine the InstGen method with maximal completion to obtain a powerful SAT-based theorem prover with dedicated support for equality. We expect that by combining the two approaches, the SAT-based approxima- tions can benefit from each other, which will result in an instantiation-based prover that integrates equational reasoning in an optimal way. Second, we expect that the two above-mentioned approaches and even more so their combination can benefit from machine learning techniques for optimizations. Thus we will implement mechanisms that allow us to learn good term orderings, strategies to choose equations, or selection strategies for literals. Finally, automated theorem provers are highly complex and thus error-prone pieces of code. Even if a proof is output, it is impossible for humans to verify its correctness. Up to now, hardly any stand-alone proof checkers exist that certify proofs from first-order provers, and no such certifier exists for instantiation-based provers. In order to enhance trustability of SAT-based provers, we will implement a trusted proof checker for the maximal completion tool as well as our instantiation-based theorem prover. In summary, this project pushes the limits of SAT-based theorem proving beyond the current frontiers in three respects: applicability to equational reasoning, flexibility, and trustability. Since SAT solvers and their variants are about to become integral parts of software components, this research is of high current relevance.

The research field of Automated Reasoning seeks to develop and implement algorithms that automate logical reasoning in a computing system. Such systems are crucial to verify that hardware and software components work as expected, or to solve planning or scheduling problems, for example. A comparatively simple case of automated reasoning deals with the Boolean satisfiability problem (SAT), i.e., the problem of determining whether there exists a variable assignment that satisfies a given Boolean formula. As an NP-complete problem, it has long been considered intractable. However, in the last two decades SAT solving has experienced an enormous performance boost: SAT solvers are now able to handle huge formulas, and routinely applied in a wide range of applications, like planning tasks and automatic hardware verification. To enhance expressiveness, SAT solvers have been extended to SMT solvers, which can also handle arithmetic and other practically relevant theories However, many application problems in automated reasoning cannot be expressed in SAT/SMT alone: more powerful inference mechanisms are needed. In this project we considered reasoning with equations, both for the purely equational case and in combination with full first-order logic. This is an important research area since equations are ubiquituous in mathematical problems and applications in verification. More precisely, in this project we leveraged the success of SAT and SMT to equational reasoning: (1) Maximal completion is an efficient and effective SAT/SMT-based approach for a special task in equational reasoning, but restricted to the case where there are only positive equations. (2) Instantiation-based theorem proving is a successful theorem proving approach for first-order logic also based on SAT, but equality handling was so far rather inefficient. In this project we combined these two methods, to take advantage from the synergies between the two SAT-encodings. The combined method was implemented in the tool maedmax and evaluated experimentally. To improve the tool's effectiveness, we exploited machine learning techniques. To this end, we implemented mechanisms that allow us to learn good strategy parameters and selection strategies for literals, and worked on relevant features in this context. Finally, automated theorem provers are highly complex and thus error-prone pieces of code. Even if a proof is output, it is often too time-consuming for humans to verify its correctness. In order to enhance trustability of the tool maedmax, we implemented a trusted proof checker for the maximal completion tool. This included formally proving correctness of the underlying algorithms in a proof assitant, i.e., dedicated software to automate and check mathematical proofs. In summary, in this project we pushed the limits of SAT-based theorem proving in three respects: applicability to equational reasoning, flexibility, and trustability. Since SAT-based approaches are becoming integral in theorem proving, this research is of high current relevance.