[Zurück]

G. Reger, M. Suda, A. Voronkov:
"Recent Improvements of Theory Reasoning in Vampire";
Vortrag: IWIL 2017 - 12th International Workshop on the Implementation of Logics, Maun, Botswana (eingeladen); 07.05.2017.

Over the past years Vampire has been progressively improving its ability to reason with quantifiers and theories. Originally theory reasoning was only via theory axioms and evaluation but over the past year two new techniques have been introduced. The first is the recent work of AVATAR modulo theories, previously presented, for ground theory reasoning. The second, the focus of this talk, consists of two new methods for reasoning with non-ground theory clauses (where we currently focus on the theory of arithmetic). The first new method is \emph{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 ~p(x+1) v q(x) to produce 2 != x+1 v 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 second new method utilises theory constraint solving (an SMT solver) to perform reasoning within a clause to find an instance where we can remove theory literals. This utilises the power of SMT solvers for theory reasoning with non-ground clauses, reasoning which is currently achieved by the addition of prolific theory axioms. Additionally, this second method can be used to discharge the constraints introduced by unification with abstraction. These methods were implemented within the Vampire theorem prover and experimental results show that they are useful for solving currently unsolved problems.

Vampire, theory reasoning