Programa de la materia

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. 


Bibliografía


Titulo/Artículo

Autor/es

Editorial/Publicación

Año de edición

Lógica Formal para Informáticos

Arenas, L.

Díaz de Santos

1996

Mathematical Logic for Computer Science

Ben-Ari, M.

Springer Verlag

2012

Logic and its Applications

Burke, E.; Foxley, E.

Prentice Hall, Series in Computer Science

1996

Apuntes de Lógica Matemática. Notas de clase

Celani, S.

Facultad Cs. Exactas, UNCPBA. http://ccomp2.alumnos.exa.unicen.edu.ar/apuntes

2003

Logic in Computer Science: Modelling and Reasoning about Systems

Huth, M.,  Ryan, M.

Cambridge University Press

2004

The Essence of Logic

Kelly, John

Prentice Hall

1997

Lógica para Informática

Pons, C.,  Rosenfeld, R., Smith, C.

EDULP Editorial de la Universidad Nacional de la Plata

2017