« SLD-résolution » : différence entre les versions

Dernière version du 28 janvier 2024 à 13:10

Définition

En programmation logique, la SLD-résolution (Sélectionné, Linéaire, Défini) est un algorithme servant à prouver une formule de logique du premier ordre à partir d'un ensemble de clauses de Horn.

Elle est basée sur une résolution linéaire, avec une fonction de sélection sur les clauses définies.

Français

SDL-résolution

Anglais

SLD resolution

Sources

Source:Wikipedia

@@ Ligne 1 : / Ligne 1 : @@
-== Domaine ==
-[[Category:Vocabulary]]
 == Définition ==
+En programmation logique, la SLD-résolution (Sélectionné, Linéaire, Défini) est un algorithme servant à prouver une formule de logique du premier ordre à partir d'un ensemble de clauses de Horn.
-En programmation logique, la SLD-résolution (SLD signifiant Sélectionné, Linéaire, Défini) est un algorithme servant à prouver une formule de logique du premier ordre à partir d'un ensemble de clauses de Horn. Elle est basée sur une résolution linéaire, avec une fonction de sélection sur les clauses définies. La SLD-résolution est mieux connue par son extension, SLDNF (NF signifiant negation as failure, la négation par l'échec), qui est l'algorithme de résolution employé par le langage Prolog.
+Elle est basée sur une résolution linéaire, avec une fonction de sélection sur les clauses définies.
-Source:
+== Français ==
+'''SDL-résolution'''
-https://fr.wikipedia.org/wiki/SLD-r%C3%A9solution
+== Anglais ==
+'''SLD resolution'''
-== Français ==
+==Sources==
-résolution SDL
-== Anglais ==
+[https://fr.wikipedia.org/wiki/SLD-r%C3%A9solution   Source:Wikipedia ]
-=== SLD resolution ===
-SLD resolution (Selective Linear Definite clause resolution) is the basic inference rule used in logic programming. It is a refinement of resolution, which is both sound and refutation complete for Horn clauses.
-<br/>
+[[Catégorie:GRAND LEXIQUE FRANÇAIS]]
-<br/>
-<br/>
-<br/>
-<br/>
-<br/>
-<br/>