Reseau inverse

Formula : É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 A := X(t_1,\dots,t_n) \mid \neg A \mid A \vee B \mid A \wedge B \mid \forall x A \mid \exists x A}

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}$

É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{}{\;\epsilon\;}\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 . \Gamma', \Delta}{\vdash A . \Gamma, \neg A . \Gamma', \Delta}\hbox{resolution} }

Règles structurelles

É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 A . \Gamma , \Delta}{\vdash \Gamma , \Delta} \hbox{(inutile, affaiblissement)} }

É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 A . \Gamma , \Delta}{\vdash A . A . \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{\vdash A . A . \Gamma , \Delta}{\vdash A . \Gamma , \Delta} \hbox{(inutile)} }

É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 \Gamma , \Gamma, \Delta}{\vdash \Gamma , \Delta} \hbox{(reutilisation de clauses)} }

É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 \Gamma , \Delta}{\vdash \Gamma.\Gamma' , \Gamma , \Delta} \hbox{(intutile, 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 \Gamma , \Delta}{\vdash \Delta} \hbox{(inutile, affaiblissement bis)} }

É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 \Gamma , \Delta \;\;\; \Gamma' , \Delta}{\vdash \Gamma . \Gamma' , \Delta}\hbox{Splitting} \hbox{(inutile, mais tres efficace en pratique)} }