En la segunda parte de la clase de hoy del curso de Razonamiento automático se estudiado cómo verificar formalmente con Isabelle/HOL la corrección de la ordenación por inserción
La correspondiente teoría se muestra a continuación
Read More “RA2013: Verificación de la ordenación por inserción con Isabell/HOL”
En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de los ejercicios de la relación 7. En dicha relación se definen funciones para recorrer árboles binarios y se demuestran con Isabelle/HOL algunas de sus propiedades.
Los ejercicios y sus soluciones se muestran a continuación
Read More “RA2013: Verificación de propiedades de recorridos en árboles binarios con Isabelle/HOL”
En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir y demostrar propiedades de tipos de datos recursivos, funciones recursivas que no son primitivas recursivas y tipos de datos con recursión cruzada.
La correspondiente teoría Isabelle/HOL se muestra a continuación
Read More “RA2013: Razonamiento por inducción estructural, general y cruzada con Isabelle/HOL”
En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir árboles binarios en Isabelle/HOL y cómo demostrar sus propiedades.
La correspondiente teoría Isabelle/HOL se muestra a continuación
Read More “RA2013: Razonamiento sobre árboles binarios con Isabelle/HOL”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha comentado las soluciones de la 5ª relación de ejercicios cuyo objetivo es automáticamente con Isabelle/HOL propiedades de programas de cuantificadores sobre listas.
Los ejercicios y sus soluciones se muestran a continuación
Read More “RA2013: Ejercicios de cuantificadores sobre listas con Isabelle/HOL”