Demostración asistida por ordenador (2010-11)
Este curso constituye una introducción al uso del sistema Isabelle/HOL para la construcción y verificación de demostraciones formales. Exploraremos su aplicación en dos áreas fundamentales: el razonamiento sobre programas funcionales y la deducción natural en los sistemas lógicos proposicional y de primer orden.
Desde el punto de vista administrativo, este curso forma parte de la oferta académica del Centro de Formación Permanente de la Universidad de Sevilla, específicamente como un curso de formación especializada.