Cláusulas de Horn y Resolución SLD

Cláusulas de Horn y Resolución SLD

1. Secuencia de literales que contiene a lo sumo uno de sus literales positivos (disyunción de literales). Esto es un ejemplo de una cláusula de Horn, y abajo se indica una fórmula como esta también puede reescribirse de forma equivalente como una implicación:

2. Cláusula ‘definite’: Cláusula de Horn con exactamente un literal positivo. Hecho: Cláusula ‘definite’ sin literales negativos. Cláusula objetivo: Sin ningún literal positivo. (consulta) antecedente → consecuente "Si es verdad el antecedente, entonces es verdad el consecuente"

   • Estructura de clúasulas de Horn en Prolog

3. Ej: Estructura de clúasulas de Horn

4. El nombre "SLD resolution" fue dado por Maarten van Emden para la regla de inferencia sin nombre introducida por Robert Kowalski. Su nombre deriva de la resolución de SL, que es a la vez sonido y refutación completa de la forma clausal sin restricciones de la lógica. "SLD" significa "SL resolution with Definite clauses".

5. Hechos Declaración, cláusula o proposición cierta o falsa, el hecho establece una relación entre objetos. Son las sentencias más sencillas. Un hecho es una fórmula atómica o átomo: p ( t 1 , . . . , t n ) e indica que se verifica la relación (predicado) p sobre los objetos (términos) t 1 , . . . , t n .

6. Reglas Implicación o inferencia lógica que deduce nuevo conocimiento, la regla permite definir nuevas relaciones apartir de otras ya existentes

7. Consultas se especifica el problema, la proposición a demostrar o el objetivo Partiendo de que los humanos son mortales y de que Sócrates es humano, deducimos que Pepito es mortal

Images and files in the map