Download PDFOpen PDF in browser

Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning

EasyChair Preprint no. 1

19 pagesDate: September 13, 2017

Abstract

This paper explores two new inference rules for reasoning with quantifiers and theories in a saturation-based first-order theorem prover. The focus here is on non-ground clauses, complementing our recent work on AVATAR modulo theories for ground theory reasoning. The current implementation focuses on complete theories, e.g. various versions of arithmetic, but we also sketch how to work with incomplete theories.

The first new rule utilises theory constraint solving (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 is currently 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 ¬p(x+1) ⋁ q(x) to produce 2 ≄ x+1 ⋁ 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.

Additionally, the first rule can be used to discharge the constraints introduced by the second. These rules were implemented within the Vampire theorem prover and experimental results show that they are useful for solving a considerable number of previously unsolved problems.

Keyphrases: automated reasoning, Avatar, AVATAR architecture, first-order logic, Satisfiability Modulo Theories, Saturation Algorithms, SMT, SMT solving, superposition calculus, theorem proving, theory reasoning, Vampire

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
@Booklet{EasyChair:1,
  author = {Giles Reger and Martin Suda and Andrei Voronkov},
  title = {Unification with Abstraction and Theory Instantiation in Saturation-based Reasoning},
  howpublished = {EasyChair Preprint no. 1},
  doi = {10.29007/hsh2},
  year = {EasyChair, 2017}}
Download PDFOpen PDF in browser