From strong amalgamability to modularity of quantifier-free interpolation

DOI10.1007/978-3-642-31365-3_12MaRDI QIDQ2908483zbMATH OpenOpenAlexFDO

Authors Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise

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

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

Abstract: The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the 'strong (sub-)amalgamation' property. Then, we provide an equivalent syntactic characterization, identify a sufficient condition, and design a combined quantifier-free interpolation algorithm capable of handling both convex and non-convex theories, that subsumes and extends most existing work on combined interpolation.

Recommendations

• Quantifier-free interpolation in combinations of equality interpolating theories
• Interpolation, amalgamation and combination (the non-disjoint signatures case)
• Modularity results for interpolation, amalgamation and superamalgamation
• Quantifier-free interpolation of a theory of arrays
• Interpolation in local theory extensions

Cited in

(8)

• Interpolation, amalgamation and combination (the non-disjoint signatures case)
• On interpolation in automated theorem proving
• Modularity results for interpolation, amalgamation and superamalgamation
• Proof tree preserving tree interpolation
• Interpolation systems for ground proofs in automated deduction: a survey
• An extension of lazy abstraction with interpolation for programs with arrays
• Quantifier-free interpolation in combinations of equality interpolating theories
• Complete instantiation-based interpolation

Describes a project that uses

Uses Software

• z3

This page was built for publication: From strong amalgamability to modularity of quantifier-free interpolation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2908483)