Razonamiento automático (2013-14)

Este curso ofrece una introducción a la verificación formal de programas utilizando el asistente de pruebas Isabelle/HOL. Partiendo de los fundamentos de la programación funcional en Isabelle, se aprenderá progresivamente a razonar sobre programas mediante técnicas automáticas y estructuradas, incluyendo el razonamiento por casos y la inducción. Estos principios se aplicarán en la práctica para verificar la corrección de algoritmos clásicos como la ordenación por inserción y por mezcla. El temario profundiza también en los pilares lógicos de la verificación, cubriendo la deducción natural en lógica proposicional y de primer orden, tanto desde una perspectiva teórica como en su implementación práctica en Isabelle. A través de un conjunto de ejercicios prácticos y un caso de estudio final sobre la compilación de expresiones, se desarrollará una sólida competencia en el uso de asistentes de pruebas para garantizar la corrección de los programas.

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.