[Back]

B. Gleiss, L. Kovacs, M. Suda:
"Splitting Proofs for Interpolation";
Talk: CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden; 2017-08-06 - 2017-08-11; in: "Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings", Springer, Lecture Notes in Computer Science / 10395 (2017), ISBN: 978-3-319-63046-5; 291 - 309.

It is known that Craig interpolants can be efficiently computed from special kind of proofs, called local or split proofs.
In this paper we focus on local proofs and describe a novel algorithm
for computing first-order interpolants from such proofs. Compared to
previous approaches to interpolation, our work generates interpolants
in full first-order logic with theories and produces interpolants that
are ``smaller" than the ones generated before. By smaller we mean,
for example, that the interpolant contains less symbols and/or literals.
Our algorithms uses splitting functions on local proofs and
computes optimized interpolants, possibly with quantifiers, wrt. to these functions.
We implemented our approach in the first-order theorem prover Vampire
and evaluated on a large number of examples coming from the
first-order proving community. Our experiments give practical evidence
that our work improves the state-of-the-art in first-order interpolation.

Craig interpolants, local proofs, interpolant extraction

http://dx.doi.org/10.1007/978-3-319-63046-5_18

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