---
_id: '2237'
abstract:
- lang: eng
  text: 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.
alternative_title:
- LNCS
article_processing_charge: No
author:
- first_name: Régis
  full_name: Blanc, Régis
  last_name: Blanc
- first_name: Ashutosh
  full_name: Gupta, Ashutosh
  id: 335E5684-F248-11E8-B48F-1D18A9856A87
  last_name: Gupta
- first_name: Laura
  full_name: Kovács, Laura
  last_name: Kovács
- first_name: Bernhard
  full_name: Kragl, Bernhard
  id: 320FC952-F248-11E8-B48F-1D18A9856A87
  last_name: Kragl
  orcid: 0000-0001-7745-9117
citation:
  ama: 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>
  apa: '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>'
  chicago: 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>.
  ieee: R. Blanc, A. Gupta, L. Kovács, and B. Kragl, “Tree interpolation in Vampire,”
    vol. 8312. Springer, pp. 173–181, 2013.
  ista: Blanc R, Gupta A, Kovács L, Kragl B. 2013. Tree interpolation in Vampire.
    8312, 173–181.
  mla: 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>.
  short: R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.
conference:
  end_date: 2013-12-19
  location: Stellenbosch, South Africa
  name: 'LPAR: Logic for Programming, Artificial Intelligence, and Reasoning'
  start_date: 2013-12-14
date_created: 2018-12-11T11:56:29Z
date_published: 2013-01-14T00:00:00Z
date_updated: 2020-08-11T10:09:42Z
day: '14'
ddc:
- '000'
department:
- _id: ToHe
doi: 10.1007/978-3-642-45221-5_13
file:
- access_level: open_access
  checksum: 9cebaafca032e6769d273f393305c705
  content_type: application/pdf
  creator: dernst
  date_created: 2020-05-15T11:10:40Z
  date_updated: 2020-07-14T12:45:34Z
  file_id: '7858'
  file_name: 2013_LPAR_Blanc.pdf
  file_size: 279206
  relation: main_file
file_date_updated: 2020-07-14T12:45:34Z
has_accepted_license: '1'
intvolume: '      8312'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Submitted Version
page: 173 - 181
project:
- _id: 25832EC2-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: S 11407_N23
  name: Rigorous Systems Engineering
publication_status: published
publisher: Springer
publist_id: '4724'
quality_controlled: '1'
scopus_import: 1
series_title: Lecture Notes in Computer Science
status: public
title: Tree interpolation in Vampire
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 8312
year: '2013'
...