Interpolation (Section 7)

def PDL.Interpolant (φ ψ θ : Formula) : Prop

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

Equations

• PDL.Interpolant φ ψ θ = (θ.voc ⊆ φ.voc ∩ ψ.voc ∧ PDL.tautology (φ.and θ.neg).neg ∧ PDL.tautology (θ.and ψ.neg).neg)

theorem PDL.interpolation {φ ψ : Formula} : tautology (φ.and ψ.neg).neg → ∃ (θ : Formula), Interpolant φ ψ θ