--- res: bibo_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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Régis foaf_name: Blanc, Régis foaf_surname: Blanc - foaf_Person: foaf_givenName: Ashutosh foaf_name: Gupta, Ashutosh foaf_surname: Gupta foaf_workInfoHomepage: http://www.librecat.org/personId=335E5684-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Laura foaf_name: Kovács, Laura foaf_surname: Kovács - foaf_Person: foaf_givenName: Bernhard foaf_name: Kragl, Bernhard foaf_surname: Kragl foaf_workInfoHomepage: http://www.librecat.org/personId=320FC952-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0001-7745-9117 bibo_doi: 10.1007/978-3-642-45221-5_13 bibo_volume: 8312 dct_date: 2013^xs_gYear dct_language: eng dct_publisher: Springer@ dct_title: Tree interpolation in Vampire@ ...