En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 5ª relación de ejercicios sobre eliminación de elementos duplicados de listas en Isabelle/HOL.
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2016: Ejercicios de eliminación de duplicados en Isabelle/HOL”
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 “RA2016: Razonamiento sobre árboles y bosques en Isabelle/HOL”
En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir en Isabelle/HOL funciones recursivas que no son primitiva recursiva y cómo demostrar propiedades de dichas funciones. Como ejemplo, se ha usado la función de Ackerman.
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2016: Funciones recursivas generales en Isabelle/HOL”
En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 4ª relación de ejercicios sobre cuantificadores sobre listas en Isabelle/HOL.
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2016: Ejercicios de cuantificadores sobre listas en Isabelle/HOL”
En la segunda parte de 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 “RA2016: Razonamiento por casos y por inducción en Isabelle/HOL”