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


m (Remplacement de texte : « ↵<small> » par «  ==Sources== »)
 
(12 versions intermédiaires par 3 utilisateurs non affichées)
Ligne 1 : Ligne 1 :
== Domaine ==
[[Category:Vocabulary]]
== Définition ==
== 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==
<h3><poll>
Choisissez parmi ces termes proposés :
SDL-résolution
résolution SLD
</poll></h3>
<h3>Discussion:</h3>
Pour le moment, le terme privilégié est «SDL-résolution».
<br/>


== 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/>

Dernière version du 28 janvier 2024 à 12: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