En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo trabajar en Isabelle/HOL con conjuntos, funciones y relaciones.
La clase se ha basado en la siguiente teoría Isabelle
Read More “RA2012: Conjuntos, funciones y relaciones”
En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo demostrar en Isabelle la corrección de un compilador de expresiones aritméticas.
La clase se ha basado en la siguiente teoría Isabelle
Read More “RA2012: Demostracción en Isabelle de la corrección de un compilador de expresiones aritméticas”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha presentado cómo definir tipos de datos mutamente recursivos y cómo demostrar propiedades por inducción cruzada sobre dichos tipos.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Recursión e inducción cruzada en Isabelle/HOL”
En la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de verificación en Isabelle de propiedades de funciones sobre listas de las siguientes relaciones:
En la clase de hoy del curso de Razonamiento automático se ha resuelto de manera colaborativa ejercicios sobre la demostración de propiedades de la función de sustitución con Isabelle/HOL. Su objetivo es ilustrar el uso del razonamiento por inducción y por casos en Isabelle. Para ca propiedad se presentan distintas demostraciones desde las automáticas a las detalladas.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Verificación de propiedades de la sustitución en Isabelle/HOL”