Reseau inverse
Syntaxe
Formules : É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}
On quotiente les formules pas les lois de De Morgan.
Clauses (à démontrer) : É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 \Gamma := 1 \mid A . \Gamma} (le point est une conjonction commutative et associative avec élément neutre)
Séquents : É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 \Delta := 0 \mid \Gamma , \Delta} (la virgule est une dicjonction commutative et associative)
Règles logiques
É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 . B . \Gamma , \Delta}{\vdash A \wedge B . \Gamma , \Delta}\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{\vdash A . \Gamma, B . \Gamma, \Delta}{\vdash A \vee B. \Gamma , \Delta}\vee_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{\vdash A . \Gamma, \Delta}{\vdash \forall x A . \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{}{\vdash 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{\vdash \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 . \Gamma, \neg A . \Gamma, \Delta}{\vdash \Gamma, \Delta}\hbox{reversed resolution} \;\;\;\hbox{(inutile, fait echouer 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 \Delta}{\vdash A . \neg A . \Gamma, \Delta}\hbox{tautology elimination} \;\;\;\hbox{(inutile)} }
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}\nu\;\;\; \hbox{(inutile, affaiblissement, 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 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{(inutile, subsumption, tres efficace en recherche de preuve)} }
É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{(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, tres efficace en recherche de preuve)} }
Tentative de Calcul
Formules : É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 + B \mid A \wedge B \mid A \times B \mid A \vee B \mid \forall x A \mid \exists x A}
Clauses (à démontrer) : É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 \Gamma := 1 \mid A^x . \Gamma}
(le point est une conjonction commutative et associative avec élément neutre)
Séquents : É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 \Delta := 0 \mid \Gamma , \Delta} (la virgule est une dicjonction commutative et associative)
Contraintes : pour tout séquent É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 \Delta} et nom de canal É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 x} , il existe au plus une 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 A} telque É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} ou É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 \neg A^x} . Pour imposer cette contrainte, on tilse des contextes de typage des canaux: É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 \gamma := x_1 : A_1, \dots, x_n : A_n} .
Definition : É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 \Delta \otimes \Delta'} : É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 (\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
É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 \times B, x:A, y : B, \gamma\vdash !z\leftarrow(x,y) : (A \times B)^z, \neg A^x, \neg B^y}\times_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, 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 }
É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, 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^x . \neg A^x . \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^x . \neg A^x . \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{\gamma \vdash t : \Delta}{\gamma \vdash t : \Gamma , \Delta}\;\;\; \hbox{weakening} }