LI2012: Tableros semánticos proposicionales

PorJosé A. Alonso

En 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:

  • F es una tautología syss \{\neg F\} es inconsistente.
  • F es consecuencia lógica de S syss S \cup \{\neg 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 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.

Como tarea pendientes se propone la resolución de los ejercicios del tema 3 del libro de ejercicios.

Las transparencias de esta clase son las del tema 3
Read More “LI2012: Tableros semánticos proposicionales”

LI2012: Deducción natural en lógica proposicional (2)

PorJosé A. Alonso

En la clase de hoy del curso Lógica Informática se ha completado el estudio de la deducción natural en lógica proposicional.

La reglas que se han visto en la clase son las de la conjunción, las de la negación, las del bicondicional y las reglas derivadas (modus tollens, introducción de la doble negación, reducción al absurdo y ley del tercio excluso).

Como tarea pendiente se propone la resolución de los ejercicios del tema 2 del libro de ejercicios.

Las transparencias de esta clase son las páginas 11-28 del tema 2
Read More “LI2012: Deducción natural en lógica proposicional (2)”