Stronger Proof Automation through Nonclausal Proof Search

Automated theorem provers are computer programs that prove mathematical statements, such as the Pythagorean theorem, without user interaction. To achieve this, most provers convert the mathematical statement to prove to a form that is easier to process by the computer, namely to so-called clauses. Such provers are called clausal. However, the conversion to clauses can significantly complicate the proof of many statements. For such cases, nonclausal provers, which do not depend on the conversion to clauses, can be a convenient solution. Although nonclausal provers possess attractive theoretical properties, they are currently scarcely researched and therefore cannot yet compete with clausal provers. We wish to research methods to make nonclausal provers stronger. Our hypothesis is that well-implemented nonclausal provers can play their strengths compared to clausal provers not only in theory, but also in practice. First, we want to verify theoretical properties of a nonclausal prover with the aid of a computer program to obtain a solid theoretical foundation for our further research. On this basis, we want to improve the efficiency of an existing nonclausal prover. Finally, we want to use the acquired insights to create a nonclausal version of one of the best clausal provers. This allows us to directly compare clausal and nonclausal provers and thus to verify our hypothesis.

Critical computer programs, such as for the control of infrastructure (vehicles, power plants, dams etc.), are subject to strong safety criteria. For example, a program controlling an automatic subway must fulfil several properties (also called *propositions*), e.g. that trains only ride with closed doors and never collide with other trains. Before such a program is employed, there have to be *proofs* that the program actually fulfils the desired propositions. However, manual verification of such proofs is error-prone and can cost human lives. Therefore, such proofs are verified using programs called *proof checkers*. This requires that the propositions as well as their proofs are present in a shape comprehensible to the proof checker. Because manual creation of such proofs is time-consuming, one can use other programs called *(automatic) theorem provers*, which find many such proofs without human intervention. The more proofs a theorem prover finds, the fewer proofs have to be created manually, reducing time and costs for the verification of critical programs. In the context of this research project we have improved the performance of theorem provers and proof checkers. First, we have researched how to increase the amount of propositions that can be proven by a *theorem prover* in given time. For this purpose we have modified an existing theorem prover. The theorem prover disposes of several heuristics for proof search. The best heuristics restrict the search space in such a way that they cannot find all theoretically existing proofs, but find more proofs in short time in practice. By chance, we have discovered a new heuristic called REX, which restricts the search space less than the previous best heuristic. For several datasets consisting of propositions stemming from practice, we have investigated how many propositions different heuristics are able to prove. For all datasets the number of found proofs increased when REX was used compared of the previous best heuristic, in one case by up to 19%. Next, we have researched how to improve the performance of *proof checkers*. Proofs that are automatically produced (e.g. by theorem provers) can frequently become quite large. Processing such large proofs by existing proof checkers can take significant amounts of time, which reduces productivity. Existing proof checkers have processed proofs sequentially. In this project, we have introduced a new design for proof checkers, which allows for the concurrent verification of multiple proofs. The challenge consisted in increasing performance while continuing to meet the rigorous correctness requirements. The resulting proof checker can verify a large amount of proofs more than seven imes as fast as the previously fastest proof checker. By our improvements of automatic theorem provers and proof checkers, the safety of critical programs can be verified faster and cheaper.