LI2011-12: Ejercicios de deducción natural y tableros semánticos proposicionales

En la clase de hoy del curso Lógica Informática se han comentados soluciones de ejercicios de deducción natural y tableros semánticos proposicionales. Los enunciados de los ejercicios se encuentran en los temas 2 y 3 del libro de ejercicios.

Las soluciones de los ejercicios de deducción natural se encuentran en aquí.

También se ha comentado los tipos de problemas de deducción natural y los tipos de problemas de tableros semánticos.

LI2011-12: Tableros semánticos proposicionales

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 “LI2011-12: Tableros semánticos proposicionales”

LI2011-12: Deducción natural en lógica proposicional (2)

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 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).

Además, se ha visto cómo usar Pandora para editar demostraciones por deducción natural.

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

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

LI2011-12: De la semántica a la deducción natural en lógica proposicional

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

De la semántica de la lógica proposicional se ha demostrado la equivalencia entre los distintos problemas semánticos:

  1. decidir si una fórmula es consecuencia lógica de un conjunto finito de as,
  2. decidir si una fórmula es una tautología,
  3. decidir si una fórmula es insatisfacible y
  4. decidir si un conjunto de fórmulas es inconsistente.

También se ha mostrado cómo usar el sistema Gateway to Logic para resolver problemas, aplicándolo al rompecabeza de los veraces y mentirosos. Finalmente, se ha comentado la relación de tipos de problemas.

Teminado el estudio semántico (cuyo problema fundamental es dado un conjunto de fórmulas S y una fórmula F, decidir si F es consecuencia de S (en notación, S |= F)), comenzamos 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, de la doble negación, de eliminación del condicional, de modus tollens, de introducción del condicional y las de la disyunción.

Como tarea pendiente se propone la resolución de los 36 primeros apartados del ejercicio 5 del tema 2 del libro de ejercicios, cuyas soluciones se encuentran en libro de ejercicios de deducción natural en lógica proposicional.

Las transparencias de esta clase son las páginas 1-12 del tema 2
Read More “LI2011-12: De la semántica a la deducción natural en lógica proposicional”