RA2014: Razonamiento sobre tipos recursivos en Isabelle/HOL
En la tercera parte de la clase de hoy del curso de Razonamiento automático se ha estudiado
- cómo definir árboles binarios en Isabelle/HOL y cómo demostrar sus propiedades,
- cómo definir y razonar con funciones recursivas que no son primitivas recursivas y
- cómo definir y razonar con tipos de datos mutuamente recursivos.
La correspondiente teoría Isabelle/HOL se muestra a continuación
Read More “RA2014: Razonamiento sobre tipos recursivos en Isabelle/HOL”