Razonamiento automático (2017-18)

El curso se centra en el razonamiento formal sobre programas y la demostración asistida por ordenador, utilizando como herramienta principal el asistente de demostración Isabelle/HOL. Partiendo de una introducción a la programación funcional, se profundiza en los fundamentos de la deducción natural, tanto proposicional como de primer orden, y se abordan diversas técnicas de razonamiento como el automático, el estructurado, por casos y por inducción. Estos métodos se aplican al análisis de estructuras de datos fundamentales como árboles y bosques, culminando con casos de estudio exhaustivos que incluyen la verificación formal de algoritmos de ordenación (por inserción y mezcla) y la compilación de expresiones, todo ello consolidado a través de ejercicios prácticos diseñados para afianzar cada concepto.

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.