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

É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[x:=t] . \Gamma, \Delta}{\vdash \exists x A . \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} }

É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 . \neg A, \Delta}{\vdash \Delta}\hbox{coupure} \hbox{(inutile, pas la propriete de la sous-formule)} }

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

É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{(inutile, subsumption, tres efficace en recherche de preuve)} }

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

É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, tres efficace en recherche de preuve)} }

Calcul

Éliminer certaines règles ???

En particulier la coupure et éventuellement les deux autres qui font échouer la propriété de la sous-formule.