Lógica Proposicional

Unidad 1 – Sintaxis de la Lógica Proposicional

Repaso de definiciones básicas: alfabeto, fórmulas, subfórmulas, longitud de una fórmula.

Unidad 2 - Semántica de la Lógica Proposicional

Repaso de conceptos básicos: valuaciones, tablas de verdad, relación entre tablas de verdad y valuaciones, equivalencia lógica, sustituciones, satisfacibilidad de fórmulas. Tautologías, contradicciones y contingencias. Árboles de Refutación. Consecuencia semántica y deducción. Propiedades de la consecuencia semántica. Teorema de la Deducción. Teorema de Compacidad.

Unidad 3 – Deducción por Resolución

Formas normales: Forma normal conjuntiva y disyuntiva de una fórmula. Cláusulas. Resolvente. Deducción por Resolución. Formalización de enunciados en lenguaje natural. Algoritmo de Davis-Putnam. Teoremas de Corrección y Completitud. Decidibilidad.  Claúsulas de Horn. Resolución lineal y unitaria. 

 

Lógica de Predicados de Primer Orden

Unidad 4 - Sintaxis de los Lenguajes de Primer Orden

Alfabeto, términos, fórmulas atómicas, fórmulas. Variables libres y ligadas. Alcance de un cuantificador. Términos libres para una variable. Sustituciones. Fórmulas cerradas.

Unidad 5 – Semántica de la Lógica de Predicados de Primer Orden

Modelos. Valor de verdad de una fórmula en un modelo: fórmula válida bajo una valuación, válida o falsa en un modelo. Fórmulas satisfacibles, lógicamente válidas y contradictorias. Árboles de refutación. Equivalencia. Consecuencia Semántica. Teorema de la Deducción. Formalización de enunciados en lenguaje natural.

Unidad 6 – Teoría de Herbrand

Forma prenexa, forma normal conjuntiva y forma clausular de una fórmula. Teorema de Skolem. Modelos de Herbrand. Teorema de Herbrand. Concepto de p-satisfacible. Determinación de validez de fórmulas.

Unidad 7 - Resolución

Sustituciones. Composición de sustituciones. Unificación. Algoritmo de Unificación de Robinson. Resolvente. Deducción por Resolución. Teoremas de Corrección y Completitud. Indecidibilidad de la lógica de primer orden. Estrategias de simplificación de conjuntos de cláusulas Resolución lineal y unitaria. 

Unidad 8 – Resolución y Programación Lógica

Cláusulas de Horn. Lógica de programas. Modelo de Herbrand de una Lógica de Programas. Sustituciones de respuesta correcta. Programación Lógica. Aplicaciones en resolución de problemas. Resolución lineal, unitaria e input resolución para cláusulas de Horn. Teoremas de Corrección y Completitud.