Sequent

Ein syntaktisches Objekt der Form Γ ⇒ Δ (wobei Γ und Δ typischerweise endliche Multimengen oder Folgen von Formeln sind), das ausdrückt, dass die Konjunktion der Formeln in Γ die Disjunktion der Formeln in Δ in einem sequentiellen Kalkül impliziert.