Source: http://ccomp2rep.alumnos.exa.unicen.edu.ar/programa
Timestamp: 2019-03-18 17:51:21+00:00

Document:
Programa de la Materia - Ciencias de la Computación II (segundo cuatrimestre)
Ciencias de la Computación II (segundo cuatrimestre)
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.
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.

References: Resolución

 Resolución 
 Resolución

 Resolución 
 resolución 
 resolución

 Resolución 
 Resolución 
 resolución