A logic L has the Craig interpolation property (CIP) if, whenever A ?B ? L, there exists a formula C such that A ? C;C ? B ? L, where C is in the “common language” of A and B. What “common language” means is situation-dependent: it can mean having shared propositional variables, or individual variables, or modal operators, or nominals, etc. Whether a logic has the CIP is an important characteristic of the logic. In addition to knowing whether a logic has the CIP, because of its applications, it is useful to be able to prove the property nstructively. Historically, constructive proofs of the CIP for L make use of a cut-free proof system for L, typically a sequent calculus or tableau system.