Lógica matemática y fundamentos (2014-15)

El curso "Lógica matemática y fundamentos" ofrece una introducción a los sistemas lógicos clásicos, estructurándose en dos bloques temáticos. El primer bloque se dedica a la lógica proposicional, donde se abordan su sintaxis y semántica, y se exploran diversos sistemas deductivos y de decisión como la deducción natural, los tableros semánticos, las formas normales y el principio de resolución, culminando con el estudio de algoritmos para el problema de la satisfacibilidad (SAT). A continuación, se estudia la lógica de primer orden, extendiendo los conceptos previos de sintaxis, semántica y los métodos de prueba a este lenguaje más expresivo, e introduciendo temas específicos como las formas normales de Skolem, los modelos de Herbrand y la resolución de primer orden. Un componente distintivo del curso es su enfoque práctico, que exige la implementación computacional de los conceptos teóricos mediante el lenguaje de programación funcional Haskell y el uso del asistente de demostración Isabelle/HOL para la construcción de pruebas formales, dotando así al estudiante de una comprensión profunda que integra el fundamento teórico con la aplicación en la formalización y automatización del razonamiento.

Se trata de una asignatura del tercer año del Grado en Matemáticas de la Universidad de Sevilla.