RA2019: Razonamiento estructurado 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 de forma estructurada con Isar.
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.
Se ha usado Isabelle para analizar detalladamente las demostraciones
poniendo de relieve los lemas usados en cada paso. Para encontralos se
ha empleado la búsqueda de teoremas (con find_theorems) y la traza
(con using [[simp_trace]]).
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2019: Razonamiento estructurado sobre programas con Isabelle/HOL”