Andrei Voronkov
University of Manchester, UK

Title

Reasoning with quantifiers and theories using saturation-based reasoning

Abstract

Until recently, first-order reasoning with quantifiers and theories was done using instantiation of quantifiers by ground terms and the subsequent use of SMT solvers on resulting ground formulas.

The AVATAR architecture for saturation-based theorem provers gives an alternative way of reasoning, based on the use of superposition calculus and processing of ground literals by SMT solvers.

We discuss an recent approach, introduced in a recent work of Giles Reger, Martin Suda and the author, which is based on extending AVATAR with two new inference rules for non-ground literals. The first new rule utilises an SMT solver to perform reasoning within a clause to find an instance where we can remove one or more theory literals.

This utilises the power of SMT solvers for theory reasoning with non-ground clauses, reasoning which was previously achieved by the addition of prolific theory axioms.

The second new rule is unification with abstraction where the notion of unification is extended to introduce constraints where theory terms may not otherwise unify, e.g. $p(2)$ may unify with $\neg p(x+1) \vee q(x)$ to produce $2 \not\cong x+1 \vee q(x)$. This abstraction is performed lazily, as needed, to allow the superposition theorem prover to make as much progress as possible without the search space growing too quickly.

The talk is based on joint work with Giles Reger and Martin Suda.