RA2019: Ejercicios de cuantificadores sobre listas en Isabelle/HOL
En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 4ª relación de ejercicios de cuantificadores sobre listas. Para cada propiedad se dan tres demostraciones en Isabelle/HOL: la primera automática, la segunda estructurada y la tercera totalmente detallada mostrando todos los lemas de HOL que se utilizan en cada paso.
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2019: Ejercicios de cuantificadores sobre listas en Isabelle/HOL”