Négation par l'échec 2136716 31191522 2008-07-01T10:48:53Z Loveless 41312 robot Modifie: [[nl:Negatie als falen]] {{Ébauche|logique}} La '''négation par l'échec''' (en anglais ''NAF'' pour ''negation as failure'', ou ''NBF'' pour ''negation by failure'') est une règle d'[[inférence]] [[logique non monotone|non monotone]] en [[programmation logique]], utilisée pour la dérivation de <math>not~p</math> à partir de l'échec de la dérivation de <math>p</math>. C'est une caractéristique importante de la programmation logique depuis les origines de [[Planner]] et de [[Prolog]]. En Prolog, la négation par l'échec est habituellement implémentée en utilisant les fonctionnalités non logiques du langage. En Prolog pur, les littéraux de négation par l'échec (littéraux négatifs) de la forme <math>not~p</math> peuvent apparaître dans le corps des [[Clause (logique)|clauses]] et peuvent être utilisés pour dériver d'autres littéraux négatifs. Par exemple, si l'on considère uniquement les quatre clauses suivantes : <math>p \leftarrow q \and not~r</math><br /> <math>q \leftarrow s</math><br /> <math>q \leftarrow t</math><br /> <math>t \leftarrow</math> La négation par l'échec dérive <math>not~s</math>, <math>not~r</math> et <math>p</math>. == Sémantique par complétion == La sémantique de la négation par l'échec est restée un problème ouvert jusqu'à ce que [[Keith Clark]] montre en 1978<ref name="klc">{{en}}Keith Clark, "Negation as Failure", ''Readings in Nonmonotonic Reasoning'', Morgan Kaufmann Publishers, 1978, pages 311-325, [http://www.doc.ic.ac.uk/~klc/neg.html abstract en ligne].</ref> qu'elle était correcte par rapport à la complétion du programme logique où, en gros, « seulement » et <math>\leftarrow</math> sont interprétés comme « si et seulement si », abrégé en « ssi » et noté <math>\equiv</math>. Par exemple, la complétion des quatre clauses précédentes est : <math>p \equiv q \and not~r</math><br /> <math>q \equiv s \or t</math><br /> <math>t \equiv true</math><br /> <math>r \equiv false</math><br /> <math>s \equiv false</math> La règle d'inférence de la négation par l'échec simule un raisonnement avec une complétion explicite, où la négation est appliquée aux deux côtés de l'équivalence et où la négation de la partie droite est distribuée sur les formules atomiques. Par exemple, pour montrer <math>not~p</math>, la négation par l'échec simule un raisonnement avec les équivalences suivantes : <math>not~p \equiv not~q \or r</math><br /> <math>not~q \equiv not~s \and not~t</math><br /> <math>not~t \equiv false</math><br /> <math>not~r \equiv true</math><br /> <math>not~s \equiv true</math><br /> Dans le cas non propositionnel, il faut étendre la complétion avec des axiomes d'égalité, pour formaliser l'hypothèse que des entités avec des noms différents sont elles-mêmes distinctes. La négation par l'échec simule ceci par l'échec de l'unification. Par exemple, si l'on considère uniquement les deux clauses suivantes : <math>p(a) \leftarrow</math><br /> <math>p(b) \leftarrow</math><br /> On dérive, avec la négation par l'échec, <math>not~p(c)</math>. La complétion du programme est : <math>p(X) \equiv X=a \or X=b</math> étendue avec les axiomes d'unicité des noms et de fermeture du domaine. La sémantique par complétion est étroitement liée à la notion de [[circonscription (logique)|circonscription]] et à l'[[hypothèse du monde fermé]]. == Sémantique auto-épistémique == La sémantique par complétion justifie l'interprétation du résultat <math>not~p</math> d'une inférence en négation par l'échec comme la négation classique <math>\neg p</math> de <math>p</math>. Cependant, Michael Gelfond a montré en [[1987]]<ref>{{en}} M. Gelfond, "On Stratified Autoepistemic Theories", ''AAAI-87 Sixth National Conference on Artificial Intelligence'', 1987, pages 207-211, [http://www.cs.ttu.edu/~mgelfond/papers/autoepistemic.pdf lire en ligne].</ref> qu'il était également possible d'interpréter <math>not~p</math> de manière littérale comme « <math>p</math> ne peut pas être montré », « <math>p</math> n'est pas connu » ou « <math>p</math> n'est pas cru », comme en [[logique auto-épistémique]]. L'interprétation auto-épistémique a été développée en [[1988]] par Gelfond et Lifschitz<ref>{{en}} M. Gelfond and V. Lifschitz, "The Stable Model Semantics for Logic Programming", ''5th International Conference and Symposium on Logic Programming'', R. Kowalski et K. Bowen (éditeurs), MIT Press, 1988, pages 1070-1080, [http://www.cs.ttu.edu/~mgelfond/papers/stable.pdf lire en ligne].</ref>, et constitue la base de l'''[[answer set programming]]''. La sémantique auto-épistémique d'un programme Prolog pur P avec la négation par l'échec sur des littéraux est obtenue en « étendant » P avec un ensemble Δ de littéraux négatifs (au sens de la négation par l'échec) exempts de variable libres tel que Δ soit [[sémantique des modèles stables|stable]] au sens où : Δ = {<math>not~p</math> | P ∪ Δ n'implique pas <math>p</math>} En d'autres termes, un ensemble d'hypothèses Δ sur ce qui ne peut pas être démontré est stable si et seulement si Δ est l'ensemble de toutes les formules qui ne peuvent véritablement pas être montrées à partir du programme P étendu à l'aide de Δ. Ici, à cause de la syntaxe simple des programmes en Prolog pur, l'implication peut être comprise simplement comme la dérivabilité à l'aide du [[modus ponens]] et de la [[substitution uniforme]], à l'exception de tout autre règle. Un programme peut avoir zéro, une ou plusieurs extensions stables. Par exemple, le programme suivant n'a aucune extension stable : <math>p \leftarrow not~p</math><br /> Celui-ci a exactement une extension stable Δ = {<math>not~q</math>} <math>p \leftarrow not~q</math><br /> Ce troisième programme a deux extensions stables Δ<sub>1</sub> = {<math>not~p</math>} et Δ<sub>2</sub> = {<math>not~q</math>}. <math>p \leftarrow not~q</math><br /> <math>q \leftarrow not~p</math><br /> L'interprétation auto-épistémique de la négation par l'échec peut être combinée avec la négation classique, comme en programmation logique étendue et en ''[[answer set programming]]''. En combinant les deux négations, on peut par exemple exprimer l'hypothèse du monde fermé : <math>\neg p \leftarrow not~p</math> Ou encore la valeur par défaut d'une proposition : <math>p \leftarrow not~\neg p</math> == Notes et références de l'article == <references/> {{Traduction/Référence|en|Negation as failure|166934991}} == Voir aussi == === Articles connexes === *[[Négation logique]] *[[SLD-résolution]] === Liens et documents externes === *{{en}}[http://www.w3.org/2004/12/rules-ws/report/ Rapport de l'atelier W3C sur les langages de règles pour l'interopérabilité], incluant des notes sur la négation par l'échec et la négation par l'échec avec portée (''scoped negation as failure''). {{Portail logique}} [[Catégorie:Logique]] [[en:Negation as failure]] [[ja:失敗による否定]] [[nl:Negatie als falen]] [[pt:Negação por falha]] [[zh:否定为失败]]