LI2011-12: Semántica de la lógica proposicional
En la clase de hoy del curso Lógica Informática se ha continuado el estudio de la semántica proposicional desde el punto de vista computacional; es decir, se ha ido definidendo los conceptos semánticos y comentando su posible implementación.
Hemos continuado con el estudio de la semántica de una fórmula planteando los problemas SAT y TAUT y presentando dos algoritmos para su solución: tablas de verdad y método de Quine.
Además, se han definidos los conceptos de equivalencia de fórmulas, modelos de conjuntos de fórmulas, conjuntos consistentes e inconsistentes y la relación de consecuencia lógica.
Se ha visto la equivalencia de los siguientes problemas
- decidir si una fórmula es consecuencia lógica de un conjunto finito de fórmulas,
- decidir si una fórmula es una tautología,
- decidir si una fórmula es insatisfacible y
- decidir si un conjunto de fórmulas es inconsistente.
Como aplicación se ha visto la decisión de la corrección de un argumento y la resolución de rompecabezas lógicos.
Como tarea pendientes se propone la resolución de los ejercios 27 a 37 del capítulo 1 del libro de ejercicios.
Las transparencias de esta clase son las páginas 14-34 del tema 1