Cálculo ProposicionalUnidad I - Lenguaje del Cálculo ProposicionalRepaso de definiciones básicas: alfabeto, fórmulas, subfórmulas, longitud de una fórmula. Unidad II - Semántica del Cálculo ProposicionalRepaso 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ónFormas 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. Cálculo de PredicadosUnidad IV - Sintaxis de los Lenguajes de Primer OrdenAlfabeto, 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 OrdenModelos. 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 HerbrandForma 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ónSustituciones. 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ógicaClá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ónEstrategias 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 ProgramasAserciones. Pre y post condiciones. Nociones básicas de corrección parcial y total de programas. Bibliografía
|