Programa de la materia

Cálculo Proposicional

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. 

Cálculo de Predicados

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.

Bibliografía

  • Abramsky, S. , Gabbay, D., Maibaum, T., Handbook of Logic in Computer Science, Oxford University Press, 1999.
  • Arenas, L. Lógica Formal para Informáticos, Díaz de Santos, 1996.
  • Ben-Ari, M. Mathematical Logic for Computer Science, Prentice Hall, Series in Computer Science 1993.
  • Burris, S. Logic for Mathematics and Computer Science, Prentice Hall, 1998.
  • Burke, E.; Foxley, E. Logic and its Applications, Prentice Hall, Series in Computer Science 1996.
  • Celani, S. Apuntes de Lógica Matemática. Notas de clase, Facultad Cs. Exactas, UNCPBA. 2003.
  • Cuena, J. “Lógica Informática”, Alianza-Madrid, 1985.
  • Gries, D. “The Science of Programming”, Springer Verlag, 1987.
  • Kelly, John. The Essence of Logic. Prentice Hall. 1997.