En la primera parte de la clase de hoy del curso de Razonamiento automático 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 “RA2019: Razonamiento sobre árboles y bosques 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 3ª relación de ejercicios de razonamiento estructurado sobre programas. 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 razonamiento estructurado sobre programas en Isabelle/HOL”
En la clase de hoy del curso de Razonamiento automático hemos profundizado en el estudio de las demostraciones por casos y por inducción. En concreto, se ha estudiado
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2019: Razonamiento por casos y por inducción en Isabelle/HOL”
En la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL de forma estructurada con Isar.
Para ello, se ha visto cómo representar en Isabelle/HOL las demostraciones de propiedades de programas estudiadas en el tema 8 del curso de Informática.
Los métodos de demostración utilizados son razonamiento ecuacional, inducción sobre los números naturales, inducción sobre listas e inducción sobre esquemas correspondientes a definiciones recursivas.
Se ha usado Isabelle para analizar detalladamente las demostraciones
poniendo de relieve los lemas usados en cada paso. Para encontralos se
ha empleado la búsqueda de teoremas (con find_theorems) y la traza
(con using [[simp_trace]]).
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2019: Razonamiento estructurado sobre programas con Isabelle/HOL”
En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 2ª relación de ejercicios de razonamiento sobre programas. Para cada propiedad se dan dos demostraciones en Isabelle/HOL: la primera automática y la segunda aplicativa detallando los pasos.
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2019: Ejercicios de razonamiento sobre programas en Isabelle/HOL”