En la primera parte de la clase de hoy del curso Lógica Informática se ha presentado un nuevo sistema deductivo: los tableros semánticos.

Hemos visto cómo los problemas de tautología y de consecuencia lógica se reducen a problemas de consistencia:

1. F es una tautología syss {¬F} es inconsistente.
2. F es consecuencia lógica de S syss S ∪ {¬F} es inconsistente.

Por tanto, para resolver ambos problemas basta con tener un procedimiento sistemático de búsqueda de modelos. Uno de dichos procedimientos es el de tableros semánticos.

Una ventaja de los tableros semánticos frente a la deducción natural es la reducción del número de reglas lo que facilita su automatización.

Además, se ha presentado el sistema Tree Proof Generator que busca automáticamente el tablero semántico correspondiente a la fórmula introducida.

En la segunda parte de la clase se han comentado la solución de los apartados 22 y 40 del ejercicio 2.5 del libro de ejercicios
Se propusieron para la próxima clase desde el ejercicio 5 al 10 del capítulo 3 del libro de ejercicios.

Las transparencias de esta clase son las del tema 3