LI2013: Equivalencia de problemas proposicionales. Deducción natural
En la primera parte de la clase de hoy del curso 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.
En la segunda parte hemos comenzado el estudio de la deducción natural proposicional. Las reglas que se han visto en la clase de hoy son las de la conjunción y de la doble negación.
Además, se ha comentado cómo formalizar en Isabelle/HOL la demostración del primer ejemplo, presentado distintas demostraciones: detallada (que sea parecida a la mostrada en las transparencias), estructurada y automática. El código de las demostraciones se encuentran en la teoría del tema 3.
Finalmente, se han comentado las soluciones de la 3º relación de ejercicios.