SLD resolution (original) (raw)
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.
| Property | Value |
|---|---|
| dbo:abstract | 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. (fr) 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. (en) Resolução SLD (resolução Seletiva Linear para cláusula definida), é a regra de inferência básica usada em lógica de programação. É um refinamento do principio da resolução, que é correta e completa para cláusulas de Horn. (pt) ВЛВ-резолю́ція (вибіркова лінійна резолюція з визначеними твердженнями), SLD-резолю́ція (англ. SLD-resolution, Selective Linear Definite clause resolution) — це елементарне правило висновування, що застосовується в логічному програмуванні. Воно є вдосконаленням резолюції, що є як правильним, так і спростувально повним для диз'юнктів Горна. (uk) |
| dbo:wikiPageExternalLink | http://www.cis.upenn.edu/~jean/gbooks/logic.html http://foldoc.org/%3FSLD+resolution https://cs.uwaterloo.ca/~david/cl/sld-gallier.pdf |
| dbo:wikiPageID | 11594091 (xsd:integer) |
| dbo:wikiPageLength | 10200 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1120918177 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Prolog dbr:Negation_as_failure dbr:Best-first_search dbr:Resolution_(logic) dbr:Robert_Kowalski dbr:Depth-first_search dbr:And-or_tree dbr:Stack_(abstract_data_type) dbr:Completeness_(logic) dbr:Horn_clause dbr:Logic_programming dbr:Breadth-first_search dbr:Jean_Gallier dbc:Logic_programming dbc:Rules_of_inference dbr:John_Alan_Robinson dbr:Rule_of_inference dbr:Soundness dbr:Search_tree dbr:Backward_reasoning dbr:Definite_clause dbr:Unification_(computing) dbr:Branch-and-bound |
| dct:subject | dbc:Logic_programming dbc:Rules_of_inference |
| gold:hypernym | dbr:Rule |
| rdf:type | yago:WikicatRulesOfInference yago:Abstraction100002137 yago:Cognition100023271 yago:Concept105835747 yago:Content105809192 yago:Idea105833840 yago:PsychologicalFeature100023100 dbo:Country yago:Rule105846054 |
| rdfs:comment | 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. (fr) 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. (en) Resolução SLD (resolução Seletiva Linear para cláusula definida), é a regra de inferência básica usada em lógica de programação. É um refinamento do principio da resolução, que é correta e completa para cláusulas de Horn. (pt) ВЛВ-резолю́ція (вибіркова лінійна резолюція з визначеними твердженнями), SLD-резолю́ція (англ. SLD-resolution, Selective Linear Definite clause resolution) — це елементарне правило висновування, що застосовується в логічному програмуванні. Воно є вдосконаленням резолюції, що є як правильним, так і спростувально повним для диз'юнктів Горна. (uk) |
| rdfs:label | SLD-résolution (fr) SLD resolution (en) Resolução SLD (pt) ВЛВ-резолюція (uk) |
| owl:sameAs | freebase:SLD resolution wikidata:SLD resolution dbpedia-fa:SLD resolution dbpedia-fr:SLD resolution dbpedia-pt:SLD resolution dbpedia-uk:SLD resolution https://global.dbpedia.org/id/3CHXC yago-res:SLD resolution |
| prov:wasDerivedFrom | wikipedia-en:SLD_resolution?oldid=1120918177&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:SLD_resolution |
| is dbo:wikiPageDisambiguates of | dbr:SLD |
| is dbo:wikiPageRedirects of | dbr:Standard_Linear_Derivation |
| is dbo:wikiPageWikiLink of | dbr:Problem_solving dbr:Prolog dbr:Resolution_(logic) dbr:Robert_Kowalski dbr:List_of_programming_language_researchers dbr:Glossary_of_artificial_intelligence dbr:Completeness_(logic) dbr:Horn_clause dbr:Logic_programming dbr:Prolog_syntax_and_semantics dbr:Curry_(programming_language) dbr:Procedural_programming dbr:Backward_chaining dbr:Model_elimination dbr:Mercury_(programming_language) dbr:Situation_calculus dbr:SLD dbr:Stable_model_semantics dbr:Standard_Linear_Derivation |
| is foaf:primaryTopic of | wikipedia-en:SLD_resolution |