On Interpolation and Symbol Elimination in Theory Extensions

In this paper we study possibilities of interpolation and symbol eliminationin extensions of a theory $\mathcal{T}_0$ with additional function symbolswhose properties are axiomatised using a set of clauses. We analyze situationsin which we can perform such tasks in a hierarchical way, relying on existingmechanisms for symbol elimination in $\mathcal{T}_0$. This is for instancepossible if the base theory allows quantifier elimination. We analyzepossibilities of extending such methods to situations in which the base theorydoes not allow quantifier elimination but has a model completion which does. Weillustrate the method on various examples