Êtes-vous un étudiant de l'EPFL à la recherche d'un projet de semestre?
Travaillez avec nous sur des projets en science des données et en visualisation, et déployez votre projet sous forme d'application sur Graph Search.
Concept
Négation par l'échec
Résumé
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 . 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 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 :
La négation par l'échec dérive , et .
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 qu'elle était correcte par rapport à la complétion du programme logique où « seulement » et sont interprétés comme « si et seulement si », abrégé en « ssi » et noté .
Par exemple, la complétion des quatre clauses précédentes est :
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 , la négation par l'échec simule un raisonnement avec les équivalences suivantes :
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 :
On dérive, avec la négation par l'échec, .
La complétion du programme est :
é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 clos.
Source officielle
À propos de ce résultat
Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.