Propositional Interpolation and Abstract Interpretation

Abstract

Algorithms for computing Craig interpolants have several applications in program verification. Though different algorithms exist, the relationship between them and the properties of the interpolants they generate are not well understood. This paper is a study of interpolation algorithms for propositional resolution proofs. We show that existing interpolation algorithms are abstractions of a more general, parametrised algorithm. Further, existing algorithms reside in the coarsest abstraction that admits correct interpolation algorithms. The strength of interpolants constructed by existing interpolation algorithms and the variables they eliminate are analysed. The algorithms and their properties are formulated and analysed using abstract interpretation.