  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.

Logic in Computer Science