Lógica matemática y fundamentos (2013-14)

El presente curso ofrece un estudio riguroso y sistemático de la lógica computacional, articulado en tres bloques fundamentales. Inicialmente, se abordan los principios de la lógica proposicional, cubriendo su sintaxis, semántica y los principales métodos de demostración como la deducción natural, los tableros semánticos y la resolución, incluyendo el análisis de algoritmos para el problema de satisfacibilidad (SAT). Posteriormente, el temario avanza hacia la lógica de primer orden, extendiendo los conceptos previos para incorporar cuantificadores, el tratamiento de formas normales de Skolem, los modelos de Herbrand y el principio de resolución generalizado. El curso culmina con una introducción a la lógica de orden superior, enfocada en su aplicación práctica a la verificación formal de programas mediante el asistente de demostración Isabelle/HOL. Transversalmente, se enfatiza la conexión entre la teoría y la práctica a través de la implementación de algoritmos lógicos en el lenguaje de programación funcional Haskell y la construcción de demostraciones formales, capacitando al estudiante para modelar problemas complejos y razonar sobre la corrección de programas.

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