Razonamiento automático (2019-20)

Este curso ofrece una introducción al razonamiento automático y la verificación formal de programas con Isabelle/HOL. El contenido abarca desde los conceptos básicos de programación funcional en Isabelle hasta técnicas avanzadas de razonamiento sobre programas, incluyendo métodos estructurados, razonamiento por casos e inducción, y el tratamiento de estructuras de datos como árboles y bosques. Se estudian los fundamentos de la lógica proposicional y de primer orden, junto con sus sistemas de deducción natural, tanto desde una perspectiva teórica como práctica con Isabelle/HOL. El curso también explora el problema de satisfacibilidad (SAT) y algoritmos como Davis-Putnam, así como reducciones entre problemas computacionales, proporcionando una base sólida para comprender las conexiones entre lógica, computación y verificación formal. Finalmente, se presentan casos de estudio concretos que ilustran la aplicación de estas técnicas en la verificación de algoritmos fundamentales como la compilación de expresiones y la ordenación por inserción.

La asignatura forma parte del Máster Universitario en Lógica, Computación e Inteligencia Artificial impartido por el Departamento de Ciencias de la Computación e Inteligencia Artificial de la Universidad de Sevilla.