Resolución en lógicas anotadas sobre birretículos

Este trabajo presenta los elementos básicos de la lógica de Primer Orden: su sintaxis y su semántica. Describimos un tipo especial de fórmula, llamado formas normales, que nos permiten automatizar los procesos; definimos las aplicaciones de sustitución y formalizamos el concepto de Resolución en el caso clásico. Luego enriquecemos el Principio de Resolución, por medio de una estrategia de refinamiento, obteniendo la Resolución Lineal, esta se define y se dan ejemplos. Se define el Principio de Resolución-SLD, que consiste de una estrategia de Resolución Lineal junto con un criterio de selección de literales, aplicado a cláusulas definidas. Se hace una presentación detallada de la semántica operacional, declarativa y de punto fijo, del Principio de Resolución-SLD y se demuestra que es un método deductivo valido y completo. Todo esto sobre lógicas de Primer Orden. Se describen las lógicas Anotadas, empleando como modelo a la lógica anotada Qτ. Se elige como conjunto de anotación la estructura de birretículo, el cual se define y se exhiben algunas propiedades; y as ́ı, se reconstruye el algoritmo de Resolución-SLD y su semántica en lógica Anotada sobre birretículos. Finalmente, se demuestra la validez y la completez del Principio de Resolución-SLD para lógicas Anotadas sobre birretículos; todo esto basado en el trabajo presentado por Komendantskaya.

• Autores: Ramírez Osorio, Ricardo Neftalí
• Tipo de recurso: Trabajo de grado de pregrado
• Fecha de publicación: 2009
• Institución: Universidad del Valle
• Repositorio: Repositorio Digital Univalle
• Idioma: spa
• OAI Identifier: oai:bibliotecadigital.univalle.edu.co:10893/23716
• Acceso en línea: https://hdl.handle.net/10893/23716
• Palabra clave: Lógica de Primer Orden; Lógica matemática; Programación lógica
• Rights: openAccess
• License: Atribución-NoComercial-SinDerivadas 4.0 Internacional (CC BY-NC-ND 4.0)