Towards interpolation in an SMT solver with integrated superposition

Interpolation is a technique for extracting intermediate formulae from a proof. It has applications in formal verification, where interpolation may enable a program analyser to discover information about intermediate program locations and states. We study interpolation in the theorem proving method DPLL(Gamma+T), which integrates tightly a superposition based prover Gamma in a DPLL(T) based SMT-solver to unite their respective strengths. We show how a first interpolation system for DPLL(Gamma+T) can be obtained from interpolation systems for DPLL, equality sharing and Gamma. We describe ongoing work on an interpolation system for Gamma, by presenting and proving complete an interpolation system for the ground case, followed by a discussion of ongoing work on an extension to the general case. Thanks to the modular design of DPLL(Gamma+T), its interpolation system can be extended easily beyond the ground case once a general interpolation system for Gamma becomes available.