Interpolation in Classical Propositional Logic
It serves as a tutorial or survey for researchers and students in logic and computer science, but does not present new results or improvements.
This paper introduces Craig interpolation and related concepts in classical propositional logic, presenting four methods for computing interpolants and discussing their size and links to circuit complexity.
We introduce Craig interpolation and related notions such as uniform interpolation, Beth definability, and theory decomposition in classical propositional logic. We present four approaches to computing interpolants: via quantifier elimination, from formulas in disjunctive normal form, and by extraction from resolution or tableau refutations. We close with a discussion of the size of interpolants and links to circuit complexity.