Interpolation in local theory extensions

In this paper we study interpolation in local extensions of a base theory. Weidentify situations in which it is possible to obtain interpolants in ahierarchical manner, by using a prover and a procedure for generatinginterpolants in the base theory as black-boxes. We present several examples oftheory extensions in which interpolants can be computed this way, and discussapplications in verification, knowledge representation, and modular reasoningin combinations of local theories.Comment: 31 pages, 1 figur