[Back]

G. Reger, M. Suda:
"Local proofs and AVATAR";
Talk: Fourth Vampire Workshop - VAMPIRE 2017, Gothenburg, Sweden; 2017-08-07.

One of the state-of-the-art approaches to generating first-order interpolants is based on processing so called local proofs and combining conclusions of color-eliminating inferences. Such an approach to interpolation can be stated in terms of assigning colors to the symbols of the signature and local proofs are those that do not mix colors in inferences. Local proofs can be obtained by instructing a first-order prover to block inferences that would violate this rule. Such a restriction in general does not preserve completeness, but local proofs are discovered in many cases.

One of the most influential improvements of first-order theorem provers of recent years is the AVATAR architecture for clause splitting. AVATAR employs a SAT solver to pick splitting branches, thus delegating the propositional essence of the given problem to the dedicated solver. This leads to a combination which has been shown to be highly successful in practice. However, the most straightforward adaptation of AVATAR to produce local proofs is quite restrictive as it does not allow the important color-eliminating inferences to happen within the first-order part of the prover.

In this paper, we explore how severely this restriction impairs the strength of AVATAR for finding local proofs in practice. We then propose and evaluate a new approach for obtaining local proofs with AVATAR which compromises on the side of clause splitting and the use of a SAT solver to allow first-order color-eliminating inferences in AVATAR.

Local proofs, AVATAR, interpolants

http://publik.tuwien.ac.at/files/publik_264642.pdf