Formula : A := X ( t 1 , … , t n ) ∣ ¬ A ∣ A ∨ B ∣ A ∧ B ∣ ∀ x A ∣ ∃ x A {\displaystyle A:=X(t_{1},\dots ,t_{n})\mid \neg A\mid A\vee B\mid A\wedge B\mid \forall xA\mid \exists xA}
Clause (à démontrer) : Γ := 1 ∣ A . Γ {\displaystyle \Gamma :=1\mid A.\Gamma } (le point est une conjonction)
Séquent : Δ := 0 ∣ Γ , Δ {\displaystyle \Delta :=0\mid \Gamma ,\Delta } (la virgule est une dicjoncyion)
