conference paper published yes Régis Blanc author Ashutosh Gupta author 335E5684-F248-11E8-B48F-1D18A9856A87 Laura Kovács author Bernhard Kragl author 320FC952-F248-11E8-B48F-1D18A9856A870000-0001-7745-9117 ToHe department LPAR: Logic for Programming, Artificial Intelligence, and Reasoning Rigorous Systems Engineering project 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. https://research-explorer.ista.ac.at/download/2237/7858/2013_LPAR_Blanc.pdf application/pdfno Springer2013Stellenbosch, South Africa eng 10.1007/978-3-642-45221-5_13 8312173 - 181 Blanc R, Gupta A, Kovács L, Kragl B. Tree interpolation in Vampire. 2013;8312:173-181. doi:<a href="https://doi.org/10.1007/978-3-642-45221-5_13">10.1007/978-3-642-45221-5_13</a> Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire. 8312, 173–181. R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181. Blanc, Régis, et al. <i>Tree Interpolation in Vampire</i>. Vol. 8312, Springer, 2013, pp. 173–81, doi:<a href="https://doi.org/10.1007/978-3-642-45221-5_13">10.1007/978-3-642-45221-5_13</a>. 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., &#38; Kragl, B. (2013). Tree interpolation in Vampire. Presented at the LPAR: Logic for Programming, Artificial Intelligence, and Reasoning, Stellenbosch, South Africa: Springer. <a href="https://doi.org/10.1007/978-3-642-45221-5_13">https://doi.org/10.1007/978-3-642-45221-5_13</a> Blanc, Régis, Ashutosh Gupta, Laura Kovács, and Bernhard Kragl. “Tree Interpolation in Vampire.” Lecture Notes in Computer Science. Springer, 2013. <a href="https://doi.org/10.1007/978-3-642-45221-5_13">https://doi.org/10.1007/978-3-642-45221-5_13</a>. 22372018-12-11T11:56:29Z2020-08-11T10:09:42Z