« Reseau inverse » : différence entre les versions
Aucun résumé des modifications |
|||
| Ligne 78 : | Ligne 78 : | ||
== Tentative de Calcul == |
== Tentative de Calcul == |
||
Formules : <math>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</math> |
|||
Clauses (à démontrer) : <math>\Gamma := 1 \mid A^x . \Gamma</math> (le point est une conjonction commutative et associative avec élément neutre) |
Clauses (à démontrer) : <math>\Gamma := 1 \mid A^x . \Gamma</math> (le point est une conjonction commutative et associative avec élément neutre) |
||
| Ligne 85 : | Ligne 88 : | ||
Contraintes : pour tout séquent <math>\Delta</math> et nom de canal <math>x</math>, il existe au plus une formule <math>A</math> |
Contraintes : pour tout séquent <math>\Delta</math> et nom de canal <math>x</math>, il existe au plus une formule <math>A</math> |
||
telque <math>A^x</math> ou <math>\neg A^x</math>. |
telque <math>A^x</math> ou <math>\neg A^x</math>. |
||
<math> |
|||
\frac{\vdash t : A^x . B^y . \Gamma_i , A^x \Gamma'_j , B^y . \Gamma''_k , \Delta} |
|||
{\vdash ?z(x,y).t : (A \vee B)^z . \Gamma_i , (A \vee B)^z . \Gamma'_j , (A \vee B)^z . \Gamma'_k , \Delta}\wedge_i |
|||
</math> |
|||
<math> |
|||
\frac{\vdash A . \Gamma, \Delta}{\vdash A \vee B. \Gamma , \Delta}\vee_i |
|||
</math> |
|||
<math> |
|||
\frac{\vdash A . \Gamma, \Delta}{\vdash \forall x A . \Gamma, \Delta}\forall_i\;\;\; (x \hbox{ non libre dans la conclusion}) |
|||
</math> |
|||
<math> |
|||
\frac{\vdash A[x:=t] . \Gamma, \Delta}{\vdash \exists x A . \Gamma, \Delta}\exists_i |
|||
</math> |
|||
<math> |
|||
\frac{}{\vdash 1}\hbox{axiom} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash \Gamma . \Gamma', \Delta}{\vdash A . \Gamma, \neg A . \Gamma', \Delta}\hbox{resolution} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash A . \Gamma, \neg A . \Gamma, \Delta}{\vdash \Gamma, \Delta}\hbox{reversed resolution} \;\;\;\hbox{(inutile, fait echouer la propriete de la sous-formule)} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash \Delta}{\vdash A . \neg A . \Gamma, \Delta}\hbox{tautology elimination} \;\;\;\hbox{(inutile)} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash A . \neg A, \Delta}{\Delta}\hbox{reversed tautology elimination} \;\;\;\hbox{(inutile, fait echouer la propriete de la sous-formule)} |
|||
</math> |
|||
== Règles structurelles== |
|||
<math> |
|||
\frac{\vdash A . \Gamma , \Delta}{\vdash \Gamma , \Delta}\nu\;\;\; \hbox{(inutile, affaiblissement, pas la propriete de la sous-formule)} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash A . \Gamma , \Delta}{\vdash A . A . \Gamma , \Delta}\;\;\; \hbox{(contraction)} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash A . A . \Gamma , \Delta}{\vdash A . \Gamma , \Delta}\;\;\; \hbox{(inutile)} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash \Gamma , \Gamma, \Delta}{\vdash \Gamma , \Delta}\;\;\; \hbox{(reutilisation de clauses)} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash \Gamma , \Delta}{\vdash \Gamma.\Gamma' , \Gamma , \Delta}\;\;\; \hbox{(inutile, subsumption, tres efficace en recherche de preuve)} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash \Delta}{\vdash \Gamma , \Delta}\;\;\; \hbox{(affaiblissement bis)} |
|||
</math> |
|||
<math> |
|||
\frac{\vdash \Gamma , \Delta \;\;\; \Gamma' , \Delta}{\vdash \Gamma . \Gamma' , \Delta}\hbox{Splitting} \;\;\; \hbox{(inutile, tres efficace en recherche de preuve)} |
|||
</math> |
|||
Version du 21 octobre 2008 à 09:45
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)} }
É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}{\Delta}\hbox{reversed tautology elimination} \;\;\;\hbox{(inutile, fait echouer 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}\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 . 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} .
É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 t : A^x . B^y . \Gamma_i , A^x \Gamma'_j , B^y . \Gamma''_k , \Delta} {\vdash ?z(x,y).t : (A \vee B)^z . \Gamma_i , (A \vee B)^z . \Gamma'_j , (A \vee B)^z . \Gamma'_k , \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, \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)} }
É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}{\Delta}\hbox{reversed tautology elimination} \;\;\;\hbox{(inutile, fait echouer 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}\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)} }