Tree Interpolation in Vampire

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.


Editor(s):
Mcmillan, Ken
Middeldorp, Aart
Voronkov, Andrei
Published in:
Logic for Programming, Artificial Intelligence, and Reasoning, 8312, 173-181
Presented at:
19th International Conference, LPAR, Stellenbosch, South Africa,, December 14-19, 2013
Year:
2013
Publisher:
Berlin, Heidelberg, Springer Berlin Heidelberg
Keywords:
Laboratories:




 Record created 2013-12-23, last modified 2018-09-13

Preprint:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)