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 in- terpolation algorithms are abstractions of a more general, parametrised algorithm. Further, existing algorithms reside in the coarsest abstrac- tion that admits correct interpolation algorithms. The strength of inter- polants constructed by existing interpolation algorithms and the vari- ables they eliminate are analysed. The algorithms and their properties are formulated and analysed using abstract interpretation.