Craig interpolation

From Wikipedia, the free encyclopedia

Depending on the type of logic being considered, the definition of Craig interpolation varies. Propositional Craig interpolation can be defined as follows:

If is a tautology and there exists a formula Z such that all propositional variables of Z occur in both X and Y, and and are tautologies, then Z is called an interpolant for . A simple example is that of P as an interpolant for P∧∨Q.

In propositional logic, the Craig interpolation lemma says that whenever an implication is a tautology, there exists an interpolant.

[edit] References

Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-568-81262-0.