CURSO : Logica para Ciencia de la Computacion
SIGLA : IIC2212
CRÉDITOS : 10
REQUISITOS : IIC1222 Programacion Avanzada;
IIC2252 Matematica Discreta
SEMESTRE : I
1. OBJETIVOS
Se presenta en este curso logicas formales que permiten: (1) modelar e implementar
diversas formas de razonamiento y procesos deductivos; (2) especificar formalmente
objetos y procesos computacionales. Se establece conexiones de estas logicas con los
fundamentos matematicos de la ciencia de la computacion y otras areas de la computacion.
Tambien se discute la implementacion computacional de los formalismos logicos
propuestos, con el proposito de representar y derivar conocimiento a traves del
computador. Se da especial importancia al uso de razonadores automatizados.
2. CONTENIDO
- Introduccion general al area. Formas de razonamiento. Representacion computacional
de conocimiento a traves de lenguajes de la logica formal.
- Repaso de logica proposional. Nocion de consecuencia logica. Consistencia de
formulas y conjuntos de formulas. Propiedades de la logica proposicional. Aplicaciones
de logica proposicional.
- Demostraciones formales por resolucion en logica proposicional. Introduccion a
OTTER.
- Introduccion a programacion en logica. Introduccion a PROLOG (proposicional).
- Sistemas de derivacion para la logica proposicional. Correccion, completidad y
compacidad.
- Introduccion a la computabilidad y a la complejidad computacional. Problema de la
parada de maquinas de Turing. NP-completidad de SAT.
- Sintaxis y semantica de la logica de predicados de primer orden. Estructuras. Teorias,
Especificaciones, Bases de conocimiento.
- Aplicaciones a bases de datos relacionales.
- Resolucion de primer orden, Programacion en logica.
- Ejemplos de otras logicas y reglas de deduccion. Abduccion, induccion, no monotonia.
- Teorias axiomatizables, recursivamente enumerables, decidibles, completas. Teoremas
de Kleene, Church-Turing, Goedel (incompletidad).
- Introduccion a logica de segundo orden, aritmetica de segundo orden y categoricidad
(Teorema de Dedekind).
- Complejidad computacional de teorias formalizadas (introduccion).
- Formalizaciones del razonamiento con sentido comun (introduccion). Conexion con
programacion en logica.
3. BIBLIOGRAFIA
Complementaria:
BERTOSSI D., Leopoldo. Logica para ciencia de la computacion. Santiago, Chile,
Eds. Universidad Catolica de Chile, 1996.
BARWISE, J. and ETCHEMENDY, J. The language of first-order logic. 3th ed.
Chicago, University Press, 1993.
FITTING, Melvin. First-order logic and automated theorem proving. 2nd ed. New
York, Springer, 1996.
REEVES, Steve and CLARKE, Michael. Logic for computer science. Harlow,
England, Addison Wesley, 1990.
SCHONING, Uwe. Logic for computer scientists. Boston, Birkhauser, 1989.
