Programa iic2212

PONTIFICIA UNIVERSIDAD CATOLICA DE CHILE ESCUELA DE INGENIERIA DEPARTAMENTO DE CIENCIA DE LA COMPUTACION

L´gica para Ciencia de la Computaci´n - IIC2212 o o Programa de Curso 1er semestre - 2008Horario c´tedra a Horario ayudant´ ıa Profesor Ayudante URL

: : : : :

Jueves m´dulos 5 y 6, sala Javier Pinto. o Mi´rcoles m´dulo 5, sala B14. e o Marcelo Arenas (marenas@ing.puc.cl). JuanReutter. http://www.ing.puc.cl/~marenas/iic2212-08/

Objetivo
Introducir al alumno a las l´gicas formales y sus aplicaciones en Ciencia de la Computaci´n. o o En particular, se analizan los casos del´gica proposicional y l´gica de primer orden, junto a sus o o m´todos formales de deducci´n y demostraci´n. Se da especial ´nfasis a la implementaci´n de estos e o o e o m´todos y al uso de razonadoresautom´ticos. A lo largo del curso, se presentar´ ejemplos que e a a permitir´n al alumno establecer conexiones entre la l´gica y otras ´reas de la computaci´n tales a o a o como bases de datos,complejidad computacional y representaci´n de conocimiento e inteligencia o artificial.

Metodolog´ ıa
El curso se basa en clases expositivas de 80 mins. cada una. Se realizar´ un promedio de 2 clases asemanales. Adem´s de las clases expositivas, durante el semestre se realizan algunas ayudant´ a ıas para reforzar o guiar el trabajo de los alumnos.

Evaluaci´n o
Se realizar´ tres interrogacionesy un examen. La nota final se calcula como N F = 0,7 · P I + a 0,3 · N E, donde P I es el promedio de las interrogaciones y N E es la nota del examen. Las fechas de las interrogaciones y el examen sonlas siguientes:

1

I1 I2 I3 Examen

: : : :

11 de Abril 16 de Mayo 20 de Junio 8 de Julio

Contenido
1. Introducci´n o 2. L´gica Proposicional o a) Sintaxis y lectura unica. ´ b)Sem´ntica. a c) Consecuencia l´gica y monoton´ o ıa. d) El problema de satisfacci´n (SAT). o e) Compacidad. 3. Demostraci´n Mec´nica de Teoremas o a a) Resoluci´n proposicional. o b) Introducci´n a Otter....