Lógica computacional
🤖 Grupo 7073
✏️ 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
Lógica proposicional: recordatorio, formas normales, resolución binaria, el problema SAT, el algoritmo DPLL (implementación de un solucionador SAT simple)
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).
El paradigma de programación lógica: formas normales, unificación, resolución binaria y fundamentos de PROLOG.
Sistemas deductivos: deducción natural , cálculo de secuentes (búsqueda y desarrollo de pruebas en Coq).