Ciencias de la Computación (plan 2013) 2022-1

Optativas, Lógica Computacional II

Lógica Computacional II.
Profesor: Miguel Carrillo Barajas.

Siguiendo el espíritu del temario oficial, este curso es una introducción a Lógicas no-clásicas con un enfoque computacional.
Cubriremos un panorama general de tres lógicas no clásicas: Lógica Modal, Lógica Temporal, y Lógica Intuicionista.
Tomaremos como hilo conductor del temario: la implementación de un Verificador de modelos de Software aplicando Lógica Temporal.

Otros temas (Lógica epistémica, Lógica dinámica, Lógica híbrida, Cálculo mu) del temario oficial se tratarán en forma básica, profundizando de acuerdo a los intereses específicos del grupo.

En este curso:
1. Analizaremos definiciones formales de conceptos básicos de Lógica Modal
(punto de partida para Lógica Temporal y Lógica Intuicionista).
2. Nos enfocaremos en el aspecto computacional de la Lógica Modal, mostrando sus ventajas en Ciencias de la Computación (CC).
3. La intención final es ver una introducción al tema de Verificación de Software.

Para experimentos de implementación de conceptos formales usaremos Haskell.
Para la introducción a Verificación de Software usaremos NuSMV, nuXmv.
Si el tiempo del curso lo permite, mencionaremos el uso básico de otras herramientas formales basadas en Lógica.

Los detalles sobre el temario, método de trabajo y evaluación se discutirán en la primera clase (si no funciona: ver su buzón de correo).

Miguel Carrillo.