LI2011: Resolución en lógica de primer orden

En la clase de hoy del curso Lógica Informática se ha presentado la resolución en la lógica de primer orden como ampliación del presentado en el tema 5 para la lógica proposicional.

Las principales diferencias se encuentran en la unificación, separación de variables y factorización.

Además, se ha presentado el sistema Prover9 que busca automáticamente dem ostraciones por resolución.

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

Las transparencias de esta clase son las del tema 11
Read More “LI2011: Resolución en lógica de primer orden”

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”