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)
Règle logique : A . B . Γ , Δ A ∧ B . Γ , Δ ∧ i {\displaystyle {\frac {A.B.\Gamma ,\Delta }{A\wedge B.\Gamma ,\Delta }}\wedge _{i}}
(le point est une conjonction)
(la virgule est une dicjoncyion)
