From Strong Amalgamability to Modularity of Quantifier Free Interpolation

The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually ob- tained as (disjoint) combinations of simpler theories, it is important to modularly re-use interpolation algorithms for the component theo- ries. 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 handling both convex and non-convex theories, that subsumes and extends most existing work on combined interpolation.