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 approximations can benefit from each other, which will result in an instantiation-based prover that offers better support for equality. 

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 is to push 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 future software components, this research is of high current relevance. 


Sarah Winkler

FWF project number




  • Completion for Logically Constrained Rewriting
    Sarah Winkler and Aart Middeldorp
    Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 108, pp. 30:1 – 30:18, 2018.

  • CoCo 2018 Participant: CeTA 2.33
    Bertram Felgenhauer, Franziska Rapp, Christian Sternagel and Sarah Winkler
    Proceedings of the 7th International Workshop on Confluence (IWC 2018),   pp. 63, 2018.

  • Infinite Runs in Abstract Completion
    Nao Hirokawa, Aart Middeldorp, Sarah Winkler, and Christian Sternagel
    Proceedings of the 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Leibniz International Proceedings in Informatics 84, pp. 19:1 – 19:16, 2017.
Nach oben scrollen