LI2015: Sintaxis y semántica de la lógica proposicional
La clase de hoy del curso Lógica Informática ha tenido dos partes.
En la primera parte se ha presentado un panorama de la lógica y sus aplicaciones a la informática.
En la segunda parte se ha explicado la sintaxis de la lógica proposicional insistiendo en el carácter inductivo del tipo de datos de las fórmulas proposicionales, del procedimiento de definiciones por recursión sobre las fórmulas y de demostración de propiedades por inducción sobre las fórmulas.
Finalmente, se ha iniciado el estudio de la semántica de la lógica proposicional como respuesta a la siguiente pregunta
- ¿cómo se puede construir un programa para que dada una fórmula decida si es verdadera?
Para responder la primera pregunta, empezamos definiendo, por recursión, el valor de verdad de una fórmula en una interpretació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.
Como tarea se ha propuesto resolver de los ejercicios 22 a 27 del capítulo 1 del libro de ejercicios (páginas 11 y 12).
Las transparencias de esta clase son las páginas 1-24 del tema 1.