LI2011: Formas normales de Skolem

En la clase de hoy del curso Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra sin cuantificadores G que sea equisatisfacible (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem.

Las transparencias de esta clase son las páginas 1 a 14 del tema 9
Read More “LI2011: Formas normales de Skolem”

LI2011: Tableros semánticos de primer orden

En la clase de hoy del curso Lógica Informática se ha presentado un nuevo sistema deductivo: los tableros semánticos de primer orden como ampliación del presentado en el tema 3 para la lógica proposicional.

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 8 del libro de ejercicios.

Las transparencias de esta clase son las del tema 8
Read More “LI2011: Tableros semánticos de primer orden”

LI2011: Deducción natural en lógica de primer orden

En la clase de hoy del curso Lógica Informática se presentado la ampliación del cálculo de deducción natural proposional para tratar los cuantificadores y las igualdades.

También se ha presentado el sistema Pandora para editar demostraciones por deducción natural.

Las transparencias de esta clase son las del tema 7 que se muestran a continuación
Read More “LI2011: Deducción natural en lógica de primer orden”