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 |