Depending on the type of logic being considered, the definition of Craig interpolation varies. It was first proved in 1957 for first-order logic by William Craig. Propositional Craig interpolation can be defined as follows:
If
X -> Y
is a tautology and there exists a formula Z such that all propositional variables of Z occur in both X and Y, and
X -> Z
and
Z -> Y
are tautologies, then Z is called an interpolant for
X -> Y.
A simple example is that of P as an interpolant for
P∧R -> P∨Q.
In propositional logic, the Craig interpolation lemma says that whenever an implication
X -> Y
is a tautology, there exists an interpolant.
Reference:
http://en.wikipedia.org/wiki/Craig_interpolation_lemma
