Vorträge und Posterpräsentationen (mit Tagungsband-Eintrag):
B. Gleiss, L. Kovacs, M. Suda:
"Splitting Proofs for Interpolation";
Vortrag: CADE 26 - 26th International Conference on Automated Deduction,
Gothenburg, Sweden;
06.08.2017
- 11.08.2017; 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;
S. 291
- 309.
Kurzfassung englisch:
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.
Schlagworte:
Craig interpolants, local proofs, interpolant extraction
"Offizielle" elektronische Version der Publikation (entsprechend ihrem Digital Object Identifier - DOI)
http://dx.doi.org/10.1007/978-3-319-63046-5_18
Elektronische Version der Publikation:
http://publik.tuwien.ac.at/files/publik_264666.pdf
Erstellt aus der Publikationsdatenbank der Technischen Universität Wien.