LI2015: Semántica de la lógica proposicional y deducción natural
En la primera parte de la clase de hoy del curso de Lógica Informática se ha demostrado 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.
A continuación, se ha comentado distintos tipos de problemas que se pueden plantear sobre la sintaxis y semántica de la lógica proposicional.
Finalmente, se ha comenzado el estudio de los cálculos deductivos (cuyo problema fundamental es dado un conjunto de fórmulas S y una fórmula F, decidir si F es deducible de S (en notación, S ⊢ F)). Además, se requiere que los cálculos sean adecuados y completos (es decir; que S ⊧ F si, y sólo si, S ⊢ F).
El primer cálculo deductivo que estudiamos es el de deducción natural. Las reglas que se han visto en la clase de hoy son las de la conjunción y de la doble negación.
En la segunda parte de la clase se han comentado las soluciones de los ejercicios 26.1, 27.1, 28, 29.2, 30.1 del capítulo 1 del libro de ejercicios. En la solución del último, se ha explicado cómo comprobar las formalizaciones usando APLI2.
Se propusieron para la próxima clase los ejercicios 32 a 37 del capítulo 1 del libro de ejercicios.
Las transparencias de esta clase son las páginas 1-5 del tema 2