From Strong Amalgamability to Modularity of Quantifier-Free Interpolation

DOI10.1007/978-3-642-31365-3_12zbMath1358.68183arXiv1203.3730OpenAlexW128646314MaRDI QIDQ2908483

Silvio Ranise, Roberto Bruttomesso, Silvio Ghilardi

Publication date: 5 September 2012

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1203.3730

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Interpolation, preservation, definability (03C40)

Related Items

Proof tree preserving tree interpolation ⋮ Interpolation systems for ground proofs in automated deduction: a survey ⋮ Modularity results for interpolation, amalgamation and superamalgamation ⋮ Complete instantiation-based interpolation ⋮ An extension of lazy abstraction with interpolation for programs with arrays ⋮ On interpolation in automated theorem proving

Uses Software

• z3