RA2015: Razonamiento automático sobre programas con Isabelle/HOL
En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.
Para ello, se ha visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Informática.
Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2015: Razonamiento automático sobre programas con Isabelle/HOL”