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) : É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é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 := 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{}{\;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 \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 , \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)} }
Calcul
Éliminer certaines règles ? On remarque le règle du $\nu$ qui n'est sans rapport avec le $\pi$-calcul ainsi que le Splitting qui ressemble à une composition parallèle pure (sans connexion)
L'élimination des tautologies à l'envers peuvent faire échouer la propriété de la sous-formule ... L'élimination de cette règles est le meilleurs candidat pour le calcul ?