### 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

#### 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.