Tree interpolation in Vampire Conference Paper


Author(s): Blanc, Régis; Gupta, Ashutosh; Kovács, Laura I; Kragl, Bernhard
Title: Tree interpolation in Vampire
Title Series: LNCS
Affiliation IST Austria
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.
Conference Title: LPAR: Logic for Programming, Artificial Intelligence, and Reasoning
Volume: 8312
Conference Dates: December 14-19, 2013
Conference Location: Stellenbosch, South Africa
ISBN: 978-3-642-45220-8
Publisher: Springer  
Date Published: 2013-01-14
Start Page: 173
End Page: 181
Sponsor: This research was partly supported by the Austrian National Research Network RiSE (FWF grants S11402-N23 and S11410-N23) and the WWTF PROSEED grant (ICT C-050).
DOI: 10.1007/978-3-642-45221-5_13
Notes: We thank Ken McMillan for the quantifier-free benchmarks.
Open access: no
IST Austria Authors
  1. Ashutosh Gupta
    16 Gupta
  2. Bernhard Kragl
    5 Kragl
Related IST Austria Work