Ciencias de la Computación (plan 2013) 2021-2

Cuarto Semestre, Lógica Computacional

Sinopsis:

Este curso proporciona una introducción a la Lógica Computacional, es decir a los métodos y conceptos de la Lógica Matemática que resultan relevantes para las Ciencias de la Computación. Al final del curso el alumno estará preparado para usar la lógica como una herramienta formal de apoyo en diversas áreas de las ciencias de la computación.

Logística:

El curso es mayormente autogestivo, empleando una sesión síncrona a la semana los días martes, antes de la cual se debera revisar el material correspondiente que se proporcionará desde la semana anterior. La ayudantía funcionará de manera similar. En el laboratorio se utilizarán los lenguajes Haskell y Prolog, así como el asistente de pruebas Coq.

Temario:

1. Lógica proposicional: recordatorio, formas normales, resolución binaria, el problema SAT, el algoritmo DPLL (implementación de un solucionador SAT simple)
2. Lógica de predicados de primer orden: aspectos sintácticos (ligado y substitución), semántica denotativa, consecuencia lógica, especificación formal (definiciones con predicados y reglas, análisis de argumentos lógicos, construcción de modelos contraejemplo).
3. El paradigma de programación lógica: formas normales, unificación, resolución binaria y fundamentos de PROLOG.
4. Sistemas deductivos: deducción natural , cálculo de secuentes (búsqueda y desarrollo de pruebas en Coq)

Las sesiones síncronas serán mediante Google Meet, iniciando el martes 2 de marzo.

La liga es: https://meet.google.com/kkv-etzm-aee

Recuerden que deben usar su dirección @ciencias para poder ingresar sin problemas. Si a pesar de esto, alguien tiene algún problema el primer día, envíe de inmediato un correo a favio@ciencias.unam.mx