Reseau inverse

Formula : $A:=X(t_{1},\dots ,t_{n})\mid \neg A\mid A\vee B\mid A\wedge B\mid \forall xA\mid \exists xA$

On quotiente les formules pas les lois de De Morgan.

Clause (à démontrer) : $\Gamma :=1\mid A.\Gamma$ (le point est une conjonction)

Séquent : $\Delta :=0\mid \Gamma ,\Delta$ (la virgule est une dicjoncyion)

Règle logique : ${\frac {A.B.\Gamma ,\Delta }{A\wedge B.\Gamma ,\Delta }}\wedge _{i}$

Échec de l’analyse (fonction inconnue « \math »): {\displaystyle \frac{A . \Gamma, B . \Gamma, \Delta}{A \vee B. \Gamma , \Delta}\vee_i <\math> <math> \frac{A . \Gamma, \Delta}{\forall x A . \Gamma, \Delta}\forall_i (x \hbox{non libre dans la conclusion}) }

${\frac {A[x:=t].\Gamma ,\Delta }{\exists xA.\Gamma ,\Delta }}\exists _{i}$