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}$. Pour imposer cette contrainte, on tilse des contextes de typage des canaux: $\gamma :=x_{1}:A_{1},\dots ,x_{n}:A_{n}$.

Definition : $\Delta \otimes \Delta '$ : $(\Gamma _{1},\ldots ,\Gamma _{n})\otimes (\Gamma '_{1},\ldots ,\Gamma '_{p})=\Gamma _{1}.\Gamma '_{1},\Gamma _{1}.\Gamma '_{2},\ldots ,\Gamma _{n}.\Gamma '_{p}$

Logical rules

${\frac {}{z:A\times B,x:A,y:B,\gamma \vdash !z\leftarrow (x,y):(A\times B)^{z},\neg A^{x},\neg B^{y}}}\times _{i}$

${\frac {x:A,y:B,\gamma \vdash t:\Delta }{z:A\vee B,\gamma \vdash ?z\rightarrow (x,y).t:\Delta [A^{x}:=(A\vee B)^{z},B^{y}:=(A\vee B)^{z}]}}\vee _{i}$

${\frac {}{z:A+B,x:A,\gamma \vdash !z\leftarrow L(x):(A+B)^{z},\neg A^{x}}}+_{i}^{L}$

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{}{z : A + B, y:B, \gamma \vdash !z\leftarrow R(y) : (A + B)^z, \neg B^y}+_i^R }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{x: A, \gamma \vdash t : \Delta \;\;\;\;\; y: B, \gamma \vdash u : \Delta'} {z: A \wedge B, \gamma\vdash ?z\rightarrow(x.t + y.u) : \Delta[A^x := (A \wedge B)^z] \otimes \Delta[B^y := (A \wedge B)^z]}\wedge_i }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{x: A, \gamma \vdash t : \Delta}{z: \forall x,A, \gamma \vdash ?z\rightarrow(x,\alpha).t : \Delta[A^x := (\forall \alpha A)^z]}\forall_i\;\;\; (\alpha \hbox{ non libre dans la conclusion}) }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{}{z : \exists x A, x : A[x:=t], \gamma \vdash \exists x A^z, \neg A[x:=t]^x}\exists_i }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{}{\gamma \vdash \emptyset : 1}\hbox{axiom} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : \Gamma . \Gamma', \Delta}{\gamma \vdash t : A^x . \Gamma, \neg A^x . \Gamma', \Delta}\hbox{resolution} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : \Delta \;\;\;\;\; \gamma \vdash u : \Delta'}{\gamma \vdash t \mid u : \Delta \otimes \Delta'}\hbox{splitting} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{x : A, \gamma \vdash t : \Delta}{\gamma \vdash \nu x.t : \Delta}\nu\;\;\; x \hbox{ not in } \Delta }

Simplification (structural) rules

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : \Delta}{\vdash t : A . \neg A . \Gamma, \Delta}\hbox{tautology elimination} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : A . \neg A . \Gamma, \Delta}{\gamma \vdash t : \Delta}\hbox{reversed tautology elimination} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : A^x . \Gamma , \Delta}{\vdash t : \Gamma , \Delta}\hbox{coweakening} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : A^x . \Gamma , \Delta}{\vdash t : A^x . A^x . \Gamma , \Delta}\hbox{reversed cocontraction} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : A^x . A^x . \Gamma , \Delta}{\gamma \vdash t : A^x . \Gamma , \Delta}\hbox{cocontraction} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : \Gamma , \Gamma, \Delta}{\gamma t : \vdash \Gamma , \Delta}\hbox{contraction} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\gamma \vdash t : \Gamma , \Delta}{\gamma \vdash t : \Gamma.\Gamma' , \Gamma , \Delta}\hbox{subsumption} }

Échec de l’analyse (SVG (MathML peut être activé via une extension du navigateur) : réponse non valide(« Math extension cannot connect to Restbase. ») du serveur « https://wikimedia.org/api/rest_v1/ » :): {\displaystyle \frac{\vdash \Delta}{\vdash \Gamma , \Delta}\;\;\; \hbox{weakening} }