Lògica de Primer Ordre (LPO)
| Professors Responsables: |
GLYN MORRILL (morrill lsi.upc.edu)
|
|
Crèdits: 6.0 (3.0 T 3.0 P 0.0 L)
| |
Departament:
LSI
|
Tipus d'assignatura
Optativa per la EI
Requisits de l'assignatura
|
IL
- Pre-requisit per la EI
|
|
|
MAC
- Pre-correquisit per la EI
|
|
Objectius docents
El objetivo de la asignatura es el de proporcionar al estudiante una
base solida de conocimientos de logica para informaticos. Para ello
se trataran en profundidad dos logicas: la logica proposicional y la
logica de primer orden, cubriendo por un lado los conocimientos mas
clasicos de logica matematica (sintaxis, semantica, poder expresivo,
sistemas deductivos, resultados de correccion y completitud) y, por
otro lado, los fundamentos para las diversas -cada vez mas abundantes-
aplicaciones de la logica en la informatica: verificacion de hardware,
verificacion de software (tipos de datos, protocolos de
comunicacion,...), inteligencia artificial, programacion logica, bases
de datos deductivas y deducion automatica.
Programa
1. Logica proposicional
Sintaxis
Semantica
- interpretatacion
- satisfaccion
- nomenclatura: modelos, satisfactibilidad, consecuencia...
Formas normales
Algoritmos de deduccion
- algoritmos "naif"; limitaciones en cuanto a complejidad
- resolucion: correccion y completitud
- algoritmos eficientes para clausulas de Horn
2. Logica de primer orden
Sintaxis
- terminos
- atomos
- cuantificacion, variables libres y ligadas
- formulas
Semantica
- interpretatacion
- satisfaccion
Sistemas formales tipo Gentzen, correccion y completitud, compacidad
Tableaux semanticos
Formas normales, Skolemizacion, forma clausal
Deduccion
- indecidibilidad
- substituciones, unificacion
- resolucion y factorizacion: correccion
- interpretaciones de Herbrand
- resolucion y factorizacion: completitud refutacional
- deduccion: procedimientos practicos de semi-decision
- refinamientos de la resolucion (C. Horn, R. unitaria,...)
Calculo de respuestas mediante resolucion
- SLD resolucion: fundamentos de la programacion logica
- Bases de datos deductivas
- Completitud de la resolucion para calculo de respuestas
Logica de primer orden con igualdad
- Igualdad explicita: los axiomas de igualdad
- Igualdad implicita: modelos de igualdad, paramodulacion
- fundamentos de la programacion funcional y logico-funcional
Avaluació
Habra un examen al final del cuatrimestre. Este examen tendra dos
partes: una parte teorica (T) y otra practica (P). La nota final (F)
se calcula de la siguiente manera. Si T y P son ambas mayores o
iguales a 4 entonces F es 0.5T + 0.5P. Si T y P son ambas "no
presentado" (NP), entonces F sera NP. En los demas casos, F sera la
minima de T y P (donde NP=0).
Bibliografia
Bibliografia bàsica
- U. Schoning Logic for Computer Scientists Birkhausen, 1989.
- M. Ben Ari Mathematical Logic for Computer Science Prentice-Hall, 1992.
- H. Enderton A Mathematical Introduction to Logic Academic Press, 1972.
- D. van Dalen Logic and Structure Springer-Verlag, 1994.
- G. Morrill Logica de primer ordre Edicions UPC. http://www.upc.edu/edicions/index.html, 2001
Bibliografia complementària
- A. Nerode, R. Shore Logic for Applications Springer-Verlag, 1993.
- C. Chang, R. Lee Symbolic Logic and Mechanical Theorem Proving Academic Press, 1973.
|
