Talks and Poster Presentations (with Proceedings-Entry):
B. Gleiss, L. Kovacs, M. Suda:
"Splitting Proofs for Interpolation";
Talk: CADE 26 - 26th International Conference on Automated Deduction,
- 2017-08-11; in: "Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings",
Lecture Notes in Computer Science / 10395
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
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.