Unificación y resolución en lógica de primer orden

Unificación y resolución en lógica de primer orden

DOCENTE

GRISSEL ANAHÍ CRUZ ARRIAGA

MATERIA

PROGRAMACION LOGICA Y FUNCIONAL-DS8

UNIDAD

UNIDAD 3 - PROGRAMACIÓN LOGICA

ALUMNO

WILSON ARAM VELAZQUEZ BALLINAS

NUMERO DE CONTROL

15270803

Algoritmo de Unificación

Sirve para determinar si una fórmula es consecuencia de un conjunto finito de hipótesis es inutilizable una vez que hemos de manejar una decena de fórmulas.

Definición 3.1.1. Sea L un lenguaje de primer orden. Una sustitución elemental es cualquier expresión de forma (x|t), donde x es un símbolo de variable y t es término de L. Si ϕ es una fórmula de L, (x|t)ϕ representa la fórmula obtenida reemplazando todas las ocurrencias libres de x en ϕ por t, es decir, (x|t)ϕ representa ahora la fórmula ϕ x t . Una sustitución elemental (x|t) es una sustitución elemental de renombramiento si t es un símbolo de variable.

Algoritmo de Resolución

La resolución de Robinson (1965) evita la generación de conjuntos de instancias básicas como exigen los métodos basados en el teorema de Herbrand. Puede ser aplicada directamente al cualquier conjunto Σ de cláusulas para sondear la insatisfacibilidad de Σ.

Definición 3.2.1. Sea L un lenguaje de primer orden. Definimos la relación ⊢rcvc entre conjuntosde cláusulas y cláusulas de L como sigue:

Axiomas.- No constan. Reglas.- Constan las siguientes: • regla de resolución, representada por rescv(σ, τ; θ) donde: ◦ σ es una cláusula de la forma λ ∨ σ1 y λ es una fórmula atómica. ◦ τ es una cláusula de la forma ¬δ ∨ τ1 y δ es una fórmula atómica. ◦ θ es una cláusula de la forma Φ(Ψσ1 ∨τ1), donde Ψ es una sustitución de renombramiento tal que Ψσ y τ no tienen s´ımbolos de variable en común y Φ es un unificador de máxima generalidad de Ψλ y δ. regla de disminución, representada por dis(σ; θ) donde: ◦ σ es una cláusula de la forma λ∨δ ∨σ1, siendo los literales λ y δ fórmulas atómicas ambas o λ c y δ c fórmulas atómicas ambas. ◦ θ es una cláusula de la forma Φλ ∨ Φσ1 y Φ es un unificador de λ y δ (si ambas son fórmulas atómicas) o de λ c y δ c (si ambas son fórmulas atómicas). Si dis(σ; θ) decimos que θ es un factor o disminución de de σ. o

Ing+Licdo:Yunior Andrés Castillo S., Monografias.com. (s. f.). Fundamentos de la programación lógica (página 2) - Monografias.com. Fundamentos. Recuperado 14 de mayo de 2021, de https://www.monografias.com/trabajos106/fundamentos-programacion-logica/fundamentos-programacion-logica2.shtml

José A. Alonso. (s. f.). LI2011-T11: Resolución en lógica de primer orden. SlideShare. Recuperado 14 de mayo de 2021, de https://www.slideshare.net/JoseAAlonso/li2011t11-resolucin-en-lgica-de-primer-orden

http://www.ugr.es/~folmedo/pdf/fundamentos_0506_cap_03.pdf

https://ccc.inaoep.mx/~esucar/Clases-MetIA/MetIA-05.pdf