Tree Interpolation in Vampire

DOI10.1007/978-3-642-45221-5_13zbMath1406.68104OpenAlexW33001676MaRDI QIDQ2870125

Ashutosh Gupta, Régis Blanc, Laura Kovács, Bernhard Kragl

Publication date: 17 January 2014

Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL: https://infoscience.epfl.ch/record/192948/files/LPAR13_Blanc.pdf

Mathematics Subject Classification ID

Interpolation, preservation, definability (03C40)

Related Items (3)

Proof tree preserving tree interpolation ⋮ SMT-based verification of program changes through summary repair ⋮ Farkas-based tree interpolation

Uses Software

• VAMPIRE
• z3

This page was built for publication: Tree Interpolation in Vampire