Tree interpolation in Vampire
Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire. 8312, 173–181.
Download
Conference Paper
| Published
| English
Scopus indexed
Author
Department
Series Title
LNCS
Abstract
We describe new extensions of the Vampire theorem prover for computing tree interpolants. These extensions generalize Craig interpolation in Vampire, and can also be used to derive sequence interpolants. We evaluated our implementation on a large number of examples over the theory of linear integer arithmetic and integer-indexed arrays, with and without quantifiers. When compared to other methods, our experiments show that some examples could only be solved by our implementation.
Publishing Year
Date Published
2013-01-14
Publisher
Springer
Volume
8312
Page
173 - 181
Conference
LPAR: Logic for Programming, Artificial Intelligence, and Reasoning
Conference Location
Stellenbosch, South Africa
Conference Date
2013-12-14 – 2013-12-19
IST-REx-ID
Cite this
Blanc R, Gupta A, Kovács L, Kragl B. Tree interpolation in Vampire. 2013;8312:173-181. doi:10.1007/978-3-642-45221-5_13
Blanc, R., Gupta, A., Kovács, L., & Kragl, B. (2013). Tree interpolation in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer. https://doi.org/10.1007/978-3-642-45221-5_13
Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation in Vampire.” Lecture Notes in Computer Science. Springer, 2013. https://doi.org/10.1007/978-3-642-45221-5_13.
R. Blanc, A. Gupta, L. Kovács, and B. Kragl, “Tree interpolation in Vampire,” vol. 8312. Springer, pp. 173–181, 2013.
Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire. 8312, 173–181.
Blanc, Régis, et al. Tree Interpolation in Vampire. Vol. 8312, Springer, 2013, pp. 173–81, doi:10.1007/978-3-642-45221-5_13.
All files available under the following license(s):
Copyright Statement:
This Item is protected by copyright and/or related rights. [...]
Main File(s)
File Name
2013_LPAR_Blanc.pdf
279.21 KB
Access Level
Open Access
Date Uploaded
2020-05-15
MD5 Checksum
9cebaafca032e6769d273f393305c705
Google Scholar