RA2013: Razonamiento por inducción estructural, general y cruzada con Isabelle/HOL
En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir y demostrar propiedades de tipos de datos recursivos, funciones recursivas que no son primitivas recursivas y tipos de datos con recursión cruzada.
La correspondiente teoría Isabelle/HOL se muestra a continuación
Read More “RA2013: Razonamiento por inducción estructural, general y cruzada con Isabelle/HOL”