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.

Members

Sarah Winkler

FWF project number

Contact

Publications

Abstract Completion, Formalized
Nao Hirokawa, Aart Middeldorp, Christian Sternagel, Sarah Winkler
Logical Methods in Computer Science,  15(3), pp. 19:1 – 19:42, 2019.

Certified Equational Reasoning via Ordered Completion
Christian Sternagel and Sarah Winkler
27th International Conference on Automated Deduction, Lecture Notes in Computer Science 11716, pp. 508 – 525, 2019.

MaedMax: A Maximal Ordered Completion Tool
Sarah Winkler, Georg Moser
Proceedings of the 9th International Joint Conference on Automated Reasoning, Lecture Notes in Artificial Intelligence 10900, pp. 472 – 480, 2018.

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.