Reseau inverse

Syntaxe

Formules : $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.

Clauses (à démontrer) : $\Gamma :=1\mid A.\Gamma$ (le point est une conjonction commutative et associative avec élément neutre)

Séquents : $\Delta :=0\mid \Gamma ,\Delta$ (la virgule est une dicjonction commutative et associative)

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 {}{\vdash 1}}{\hbox{axiom}}$

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

${\frac {\vdash A.\Gamma ,\neg A.\Gamma ,\Delta }{\vdash \Gamma ,\Delta }}{\hbox{reversed resolution}}\;\;\;{\hbox{(inutile, fait echouer la propriete de la sous-formule)}}$

${\frac {\vdash \Delta }{\vdash A.\neg A.\Gamma ,\Delta }}{\hbox{tautology elimination}}\;\;\;{\hbox{(inutile)}}$

${\frac {\vdash A.\neg A,\Delta }{\Delta }}{\hbox{reversed tautology elimination}}\;\;\;{\hbox{(inutile, fait echouer la propriete de la sous-formule)}}$

Règles structurelles

${\frac {\vdash A.\Gamma ,\Delta }{\vdash \Gamma ,\Delta }}\nu \;\;\;{\hbox{(inutile, affaiblissement, pas la propriete de la sous-formule)}}$

${\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{(reutilisation de clauses)}}$

${\frac {\vdash \Gamma ,\Delta }{\vdash \Gamma .\Gamma ',\Gamma ,\Delta }}\;\;\;{\hbox{(inutile, subsumption, tres efficace en recherche de preuve)}}$

${\frac {\vdash \Delta }{\vdash \Gamma ,\Delta }}\;\;\;{\hbox{(affaiblissement bis)}}$

${\frac {\vdash \Gamma ,\Delta \;\;\;\Gamma ',\Delta }{\vdash \Gamma .\Gamma ',\Delta }}{\hbox{Splitting}}\;\;\;{\hbox{(inutile, tres efficace en recherche de preuve)}}$

Tentative de Calcul

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

Clauses (à démontrer) : $\Gamma :=1\mid A^{x}.\Gamma$ (le point est une conjonction commutative et associative avec élément neutre)

Séquents : $\Delta :=0\mid \Gamma ,\Delta$ (la virgule est une dicjonction commutative et associative)

Contraintes : pour tout séquent $\Delta$ et nom de canal $x$, il existe au plus une formule $A$ telque $A^{x}$ ou $\neg A^{x}$.

${\frac {\vdash t:A^{x}.B^{y}.\Gamma _{i},A^{x}\Gamma '_{j},B^{y}.\Gamma ''_{k},\Delta }{\vdash ?z(x,y).t:(A\vee B)^{z}.\Gamma _{i},(A\vee B)^{z}.\Gamma '_{j},(A\vee B)^{z}.\Gamma '_{k},\Delta }}\wedge _{i}$

${\frac {\vdash A.\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 {}{\vdash 1}}{\hbox{axiom}}$

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

${\frac {\vdash A.\Gamma ,\neg A.\Gamma ,\Delta }{\vdash \Gamma ,\Delta }}{\hbox{reversed resolution}}\;\;\;{\hbox{(inutile, fait echouer la propriete de la sous-formule)}}$

${\frac {\vdash \Delta }{\vdash A.\neg A.\Gamma ,\Delta }}{\hbox{tautology elimination}}\;\;\;{\hbox{(inutile)}}$

${\frac {\vdash A.\neg A,\Delta }{\Delta }}{\hbox{reversed tautology elimination}}\;\;\;{\hbox{(inutile, fait echouer la propriete de la sous-formule)}}$

Règles structurelles

${\frac {\vdash A.\Gamma ,\Delta }{\vdash \Gamma ,\Delta }}\nu \;\;\;{\hbox{(inutile, affaiblissement, pas la propriete de la sous-formule)}}$

${\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{(reutilisation de clauses)}}$

${\frac {\vdash \Gamma ,\Delta }{\vdash \Gamma .\Gamma ',\Gamma ,\Delta }}\;\;\;{\hbox{(inutile, subsumption, tres efficace en recherche de preuve)}}$

${\frac {\vdash \Delta }{\vdash \Gamma ,\Delta }}\;\;\;{\hbox{(affaiblissement bis)}}$

${\frac {\vdash \Gamma ,\Delta \;\;\;\Gamma ',\Delta }{\vdash \Gamma .\Gamma ',\Delta }}{\hbox{Splitting}}\;\;\;{\hbox{(inutile, tres efficace en recherche de preuve)}}$