En la segunda parte de la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir en Isabelle/HOL conjuntos y relaciones inductivas y cómo demostrar sus propiedades.
La clase se ha basado en la siguiente teoría Isabelle
Read More “LMF2018: Definiciones inductivas en Isabelle/HOL”
En la primera parte de la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo definir y razonar en Isabelle/HOL tipos de datos recursivos como árboles binarios, árboles generales y bosques. En su definición se usa recursión cruzada y en la demostración de sus propiedades se usa inducción doble.
La teoría utilizada es la siguiente
Read More “LMF2018: Razonamiento sobre árboles y bosques en Isabelle/HOL”