Razonamiento automático (2016-17)

El curso es una introducción teórico-práctica a las técnicas de verificación formal y deducción lógica asistidas por ordenador, con un enfoque en el uso de Isabelle/HOL. A lo largo del curso se abordan temas como la programación funcional en Isabelle, el razonamiento automático y estructurado sobre programas escritos en Haskell e Isabelle/HOL, y diversas técnicas de prueba como el razonamiento por casos, por inducción y sobre estructuras como árboles y bosques. Además, se estudian casos prácticos de verificación de algoritmos clásicos, como la ordenación por inserción y por mezcla, y la compilación de expresiones. El curso también cubre fundamentos de lógica, incluyendo deducción natural tanto proposicional como en lógica de primer orden, y su implementación en Isabelle/HOL. Las sesiones prácticas están organizadas en una serie de relaciones de ejercicios que permiten aplicar los conceptos teóricos en problemas concretos, reforzando la comprensión y el dominio de las herramientas formales.

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.