LMF2019: Definiciones inductivas en Isabelle/HOL
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 dado mediante videoconferencia y el vídeo correspondiente es
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2019: Definiciones inductivas en Isabelle/HOL”