Cláusula de Horn y Resolucion SLD

Presentación

Cláusulas de Horn

Resolucion SLD

Tecnológico Nacional De México Campus Acayucan Carrera: Ingeniería En Sistemas Computacionales Grupo: 803 C Asignatura: Programación Lógica y Funcional Unidad 3: Programación lógica. Practica 10 Presentacion Nombre del estudiante: Marcela Ivette Lechuga Márquez 190B0174 Nombre del docente: MTI. Pamela Lizette Guadalupe Cerdán Valdez Fecha de entrega: 17 de mayo 2023

Cláusulas de Horn y Resolucion SLD

Programacion lógica

Cláusulas de Horn

Una cláusula de Horn (o definida) es una disyunción de literales, es decir una secuencia de literales que contiene a lo sumo un literal positivo.Las cláusulas de Horn trabajan con secuencias de literales en vez de conjuntos, esto implica dos cosas:● Los literales pueden aparecer repetidos en el cuerpo. ● Un orden en los literales del cuerpo (podemos hablar del primer literal, segundo literal, etc.). Al escribirla en notación de Kowalski tendría una de estas cuatro formas:

Cláusula Horn

Los hechos y las reglas se denominan cláusulas definidas: ➔Los hechos representan "hechos acerca de los objetos" (de nuestro universo de discurso), relaciones elementales entre estos objetos. ➔Las reglas expresan relaciones condicionales entre los objetos, dependencias, engloban todos los casos en el siguiente sentido:

• Un hecho es una regla con cuerpo vacío
• Un objetivo es una regla con cabeza vacía
• y el éxito es una regla con cabeza y cuerpo vacíos

Cláusula de Horn

• Una cláusula de Horn sin ningún literal positivo es a veces llamada cláusula objetivo (goal) o consulta (query), especialmente en programación lógica.Una fórmula de Horn es una cadena textual (string) de cuantificadores existenciales o universales seguidos por una conjunción de cláusulas de horn.Una fórmula de Horn puede escribirse como:

Hechos interesantes a destacar sobre las cláusulas de Horn

• Las cláusulas de Horn tienen el mismo poder de cómputo que la máquina de Turing o el λ – cálculo (i.e., la máquina universal). Permiten por tanto programar cualquier función computable.
• Para muchas aplicaciones de la lógica basta con restringirse a las cláusulas de Horn.
• Muchos métodos de resolución de problemas desarrollados en el campo de la inteligencia artificial pueden considerarse como modelos orientados a ser expresados también mediante cláusulas de Horn.
• A un programa definido (o simplemente programa lógico) se le conoce cómo un conjunto de cláusulas de Horn con cabeza.

Resolución SLD

Resolución SLD

La resolución SLD ( resolución de cláusula definida lineal selectiva ) es la regla de inferencia básica utilizada en la programación lógica . Es un refinamiento de la resolución , que es a la vez sólida y refutación completa para las cláusulas Horn

Resolución SLD

En el caso más simple, en lógica proposicional, los átomos y son idénticos, y la sustitución unificadora es vacía. Sin embargo, en el caso más general, la sustitución unificadora es necesaria para que los dos literales sean idénticos

https://www.youtube.com/watch?v=IK4JJ4xtGPA

Este video contiene la explicacion de un arbol de resolución SLD

¡GRACIAS!

Marcela Lechuga