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$

Syntaxe

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ègles logiques

${\frac {\vdash A.B.\Gamma ,\Delta }{\vdash A\wedge B.\Gamma ,\Delta }}\wedge _{i}$

${\frac {\vdash A.\Gamma ,B.\Gamma ,\Delta }{\vdash A\vee B.\Gamma ,\Delta }}\vee _{i}$

${\frac {\vdash A.\Gamma ,\Delta }{\vdash \forall xA.\Gamma ,\Delta }}\forall _{i}(x{\hbox{ non libre dans la conclusion}})$

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

${\frac {}{\epsilon }}axiom$

${\frac {\Gamma .\Gamma ',\Delta }{\vdash A.\Gamma ,\neg A.\Gamma ',\Delta }}$

Règles structurelles

${\frac {\vdash A.\Gamma ,\Delta }{\vdash \Gamma ,\Delta }}{\hbox{(inutile, affaiblissement)}}$

${\frac {\vdash A.\Gamma ,\Delta }{\vdash A.A.\Gamma ,\Delta }}{\hbox{(contraction)}}$

${\frac {\vdash A.A.\Gamma ,\Delta }{\vdash A.\Gamma ,\Delta }}{\hbox{(inutile)}}$

${\frac {\vdash \Gamma ,\Gamma ,\Delta }{\vdash \Gamma ,\Delta }}{\hbox{(réutilisation de clauses)}}$

${\frac {\vdash \Gamma ,\Delta }{\vdash \Gamma ,\Gamma ,\Delta }}(intutile,unepartiedelasubsumption)$

${\frac {\vdash \Gamma ,\Delta }{\vdash \Delta }}(inutile,affaiblissementbis)$

Échec de l’analyse (fonction inconnue « \hspace »): {\displaystyle \frac{\vdash \Gamma , \Delta \hspace{1cm} \Gamma' , \Delta}{\vdash \Gamma . \Gamma' , \Delta}Splitting (inutile, mais très efficace en pratique) }