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

T789

Contact

sarah winkler at uibk dot ac dot at

Publications

Infinite Runs in Abstract Completion
Nao Hirokawa, Aart Middeldorp, Sarah Winkler, Christian Sternagel
2nd International Conference on Formal Structures for Computation and Deduction, Leibniz International Proceedings in Informatics 84, pp. 19:1-19:16, 2017.