Negation par l'echec

Negation par l'echec

Négation par l'échec

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 non monotone en programmation logique, utilisée pour la dérivation de not~p à partir de l'échec de la dérivation de p. 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 not~p peuvent apparaître dans le corps des 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 :

p \leftarrow q \and not~r
q \leftarrow s
q \leftarrow t
t \leftarrow

La négation par l'échec dérive not~s, not~r et p.

Sommaire

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[1] qu'elle était correcte par rapport à la complétion du programme logique où, en gros, « seulement » et \leftarrow sont interprétés comme « si et seulement si », abrégé en « ssi » et noté \equiv.

Par exemple, la complétion des quatre clauses précédentes est :

p \equiv q \and not~r
q \equiv s \or t
t \equiv true
r \equiv false
s \equiv false

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 not~p, la négation par l'échec simule un raisonnement avec les équivalences suivantes :

not~p \equiv not~q \or r
not~q \equiv not~s \and not~t
not~t \equiv false
not~r \equiv true
not~s \equiv true

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 :

p(a) \leftarrow
p(b) \leftarrow

On dérive, avec la négation par l'échec, not~p(c).

La complétion du programme est :

p(X) \equiv X=a \or X=b

é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 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 not~p d'une inférence en négation par l'échec comme la négation classique \neg p de p. Cependant, Michael Gelfond a montré en 1987[2] qu'il était également possible d'interpréter not~p de manière littérale comme « p ne peut pas être montré », « p n'est pas connu » ou « p 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[3], 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 stable au sens où :

Δ = {not~p | P ∪ Δ n'implique pas p}

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 :

p \leftarrow  not~p

Celui-ci a exactement une extension stable Δ = {not~q}

p \leftarrow  not~q

Ce troisième programme a deux extensions stables Δ1 = {not~p} et Δ2 = {not~q}.

p \leftarrow  not~q
q \leftarrow  not~p

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é :

\neg p \leftarrow not~p

Ou encore la valeur par défaut d'une proposition :

p \leftarrow not~\neg p

Notes et références de l'article

  1. (en)Keith Clark, "Negation as Failure", Readings in Nonmonotonic Reasoning, Morgan Kaufmann Publishers, 1978, pages 311-325, abstract en ligne.
  2. (en) M. Gelfond, "On Stratified Autoepistemic Theories", AAAI-87 Sixth National Conference on Artificial Intelligence, 1987, pages 207-211, lire en ligne.
  3. (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, lire en ligne.
  • (en) Cet article est partiellement ou en totalité issu d’une traduction de l’article de Wikipédia en anglais intitulé « Negation as failure ».

Voir aussi

Articles connexes

Liens et documents externes

  • Portail de la logique Portail de la logique
Ce document provient de « N%C3%A9gation par l%27%C3%A9chec ».

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Negation par l'echec de Wikipédia en français (auteurs)

Игры ⚽ Нужно решить контрольную?

Regardez d'autres dictionnaires:

  • Négation par l'échec — 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 non monotone en programmation logique, utilisée pour la dérivation de à partir de l échec de la dérivation de p. C est… …   Wikipédia en Français

  • Negation as failure — Négation par l échec 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 non monotone en programmation logique, utilisée pour la dérivation de à partir de l échec de la… …   Wikipédia en Français

  • Negation by failure — Négation par l échec 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 non monotone en programmation logique, utilisée pour la dérivation de à partir de l échec de la… …   Wikipédia en Français

  • négation — [ negasjɔ̃ ] n. f. • negatiun XII e; lat. negatio, de negare « nier » 1 ♦ Acte de l esprit qui consiste à nier, à rejeter un rapport, une proposition, une existence; expression de cet acte. Négation de Dieu. Négation de la vérité, des valeurs. ⇒… …   Encyclopédie Universelle

  • Negation du genocide armenien — Négation du génocide arménien Cet article présente le point de vue des personnes niant ou remettant en cause le génocide arménien, ainsi que la situation en Turquie à cet égard. Sommaire 1 Contestation de la qualification de génocide 1.1 Le débat …   Wikipédia en Français

  • Négation du génocide arménien — Cet article présente le point de vue des personnes niant ou remettant en cause le génocide arménien, ainsi que la situation en Turquie à cet égard. Sommaire 1 Contestation de la qualification de génocide 1.1 Le débat entre Guenter Lewy et Vahakn… …   Wikipédia en Français

  • DIEU - La négation de Dieu — L’affirmation est un acte simple; visant intentionnellement un donné de l’expérience, sujet d’une proposition, elle lui confère les attributs qui lui reviennent; pré interrogative, l’existence de cet homme, de cet arbre, de cette maison fait… …   Encyclopédie Universelle

  • 2011 par pays en Afrique — Années : 2008 2009 2010  2011  2012 2013 2014 Décennies : 1980 1990 2000  2010  2020 2030 2040 Siècles : XXe siècle  XXIe siècl …   Wikipédia en Français

  • Démonstration par l'absurde — Raisonnement par l absurde Voir « apagogie » sur le Wiktionnaire …   Wikipédia en Français

  • Preuve par l'absurde — Raisonnement par l absurde Voir « apagogie » sur le Wiktionnaire …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”