LI2015: Semántica de la lógica proposicional
El objetivo fundamental de primera parte de la clase de hoy del curso Lógica Informática ha consistido en responder estas dos preguntas:
- ¿cómo se puede construir un programa para que dada una fórmula decida si es verdadera?
- ¿cómo se puede construir un programa para que dada un conjunto de fórmulas S una fórmula F decida si es consecuencia de S?
Para responder a la primera pregunta, desarrollamos la semántica de la lógica proposicional. En primer lugar, el valor de verdad de una fórmula en una interpretación se define por recursión. A partir del valor de verdad podemos, dada una fórmula F, dividir las interpretaciones entre las que son modelo de F y las que no lo son. Además, las fórmulas pueden clasificarse en satisfacibles (las que tienen modelos) e insatisfacibles (en caso contrario). Las fórmulas satisfacibles se pueden clasificar en tautologías (para las que todas las interpretaciones son modelo) y contingentes (en caso contrario).
Hemos continuado 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.
En la segunda parte de la clase se han comentado las soluciones de los ejercicios 22, 23, 24.1 y 25 del capítulo 1 del libro de ejercicios. Se propusieron para la próxima clase los ejercicios 26 a 31.
Las transparencias de esta clase son las páginas 14-34 del tema 1