LMF2019: Desarrollo de teorías formalizadas con Isabelle/HOL
En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo desarrollar en Isabelle/HOL teorías axiomáticas usando entornos locales (“locales”) y clases de tipos (“class”). Se ha aplicado al desarrollo de las teorías de grupos y a las de órdenes. videoconferencia.
La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:
- Primera parte:
- Segunda parte:
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2019: Desarrollo de teorías formalizadas con Isabelle/HOL”