From Strong Amalgamability to Modularity of Quantifier-Free Interpolation

TL;DR

This paper establishes a theoretical foundation for modular quantifier-free interpolation in combined theories, introducing a new condition based on strong amalgamability and providing an extended interpolation algorithm.

Contribution

It identifies strong amalgamability as a key property for modular interpolation and develops a comprehensive combined algorithm that handles both convex and non-convex theories.

Findings

Strong amalgamability is necessary and sufficient for modular quantifier-free interpolation.

The proposed algorithm extends existing methods to handle a broader class of theories.

The approach unifies and generalizes previous combined interpolation techniques.

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.