def Interpolant (φ ψ θ : Formula) : Prop

Equations

• Interpolant φ ψ θ = (Tautology (φ↣θ) ∧ Tautology (θ↣ψ) ∧ HasVocabulary.voc θ ⊆ HasVocabulary.voc φ ∩ HasVocabulary.voc ψ)

theorem tautImp_iff_TNOdenotUnsat {φ ψ : Formula} {X : TNode} : X = ({φ}, {~ψ}) → (Tautology (φ↣ψ) ↔ ¬HasSat.Satisfiable X)

theorem interpolation {ϕ ψ : Formula} : Tautology (ϕ↣ψ) → ∃ (θ : Formula), Interpolant ϕ ψ θ