WARNING:
JavaScript is turned OFF. None of the links on this concept map will
work until it is reactivated.
If you need help turning JavaScript On, click here.
Este Cmap, tiene información relacionada con: sld y horn, Resolución SLD . Hay una función de selección que selecciona un átomo del resolvente a quien aplicar resolución, Resolución SLD Es un caso particular de la resolución general, donde se cumple que El nombre "SLD resolution" fue dado por Maarten van Emden para la regla de inferencia sin nombre introducida por Robert Kowalski. Que significa Resolución Lineal con función de Selección para Cláusulas Definidas., Resolución SLD . para todo i ∈ {0, ..., k − 1}, Gi+1 de obtiene a partir de Gi “resolviendo” (en el sentido de la resolución general) el literal L = fs (Gi) con una variante de una regla de P, Tiene, pues, el siguiente aspecto . p(t1, . . . ,tn) ←, Cláusula de Horn Al escribirla en notación de Kowalski tendrá una de estas cuatro formas Éxito : ←, Cláusula de Horn Al escribirla en notación de Kowalski tendrá una de estas cuatro formas Hecho : p ←, Cláusula de Horn Al escribirla en notación de Kowalski tendrá una de estas cuatro formas representan relaciones elementales entre estos objetos, Hecho : p ← . Cláusula definida, : ← q1, . . . , qn . Objetivo definido, Cláusula de Horn Al escribirla en notación de Kowalski tendrá una de estas cuatro formas Donde <p> es la cabeza y <← q1, . . . , qn> el cuerpo), Cláusula de Horn Predicados y programas lógicos Tiene, pues, el siguiente aspecto, Cláusula de Horn Al escribirla en notación de Kowalski tendrá una de estas cuatro formas expresan relaciones condicionales entre los objetos, dependencias., Regla : p ← q1, . . . , qn . Cláusula definida, Cláusula de Horn Ejemplo en sintaxis de Edimburgo Hechos: luis) ←, Reglas: {hombre(juan) ←, hombre(luis) ←, hijo_de(juan, padre(x,y) ← hombre(x), hijo_de(y,x)} Pregunta o meta: ← padre(luis, juan), Resolución SLD Una definición formal sería Sea un programa lógico P, un par de objetivos G y G', y una función de selección fs. Una derivación de G a G' con SLD-resolución (P ∪ {G} ├SLD G') es una secuencia de objetivos G0,G1, . . . ,Gk tal que, Cláusula de Horn . Es una secuencia de literales que contiene a lo sumo un literal positivo, Tiene, pues, el siguiente aspecto . p(u1, . . . , un) ← q1 (. . .), . . . , qm(. . .), Tiene, pues, el siguiente aspecto . p(s1, . . . ,sn) ←, Resolución SLD Corección y completitud de la SLD-resolución Completitud: Sea θ una respuesta correcta para P ∪ {G}, entonces existe una SLD-refutación de G a partir de P con una secuencia de unificadores θ1, . . . , θn tal que θ = (θ1 . . . θn) |var (G), Cláusula de Horn Al escribirla en notación de Kowalski tendrá una de estas cuatro formas : ← q1, . . . , qn