Unidad I - Lenguaje del Cálculo Proposicional
Repaso de definiciones básicas: alfabeto, fórmulas, subfórmulas, longitud de una fórmula.
Unidad II - Semántica del Cálculo 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. Teorema de la Deducción. Teorema de Compacidad.
Unidad III – Deducción por Resolución
Formas normales: Forma normal conjuntiva y disyuntiva de una fórmula. Cláusulas. Resolvente. Deducción por Resolución. Algoritmo de Davis-Putnam. Teoremas de Corrección y Completitud . Decidibilidad. Claúsulas de Horn. Resolución unitaria.
Unidad IV - 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 V – Semántica en el Cálculo de Predicados de Primer Orden
Modelos. Ejemplos de 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 VI – 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 VII - 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.
Unidad VIII – 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.
Unidad IX - Refinamientos de resolución
Estrategias de simplificación de conjuntos de cláusulas. Resolución lineal y unitaria. Resolución lineal, unitaria e input resolución para cláusulas de Horn. Teoremas de Corrección y Completitud.
Unidad X – Verificación Formal de Programas
Aserciones. Pre y post condiciones. Nociones básicas de corrección parcial y total de programas.