Interpolation (Section 7)

def Interpolant (φ ψ θ : Formula) : Prop

An interpolant θ for φ and ψ only uses the vocabulary in both, is implied by φ and implies ψ.

Equations

• Interpolant φ ψ θ = (θ.voc ⊆ φ.voc ∩ ψ.voc ∧ φ⊨θ ∧ θ⊨ψ)

theorem interpolation (φ ψ : Formula) : φ⊨ψ → ∃ (θ : Formula), Interpolant φ ψ θ