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 “RA2017: 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 “RA2017: Razonamiento por casos y por inducción 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 3ª relación de ejercicios sobre razonamiento detallado sobre programas en Isabelle/HOL
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2017: Ejercicios de razonamiento detallado sobre programas 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.
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.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2017: Razonamiento estructurado sobre programas con Isabelle/HOL”
En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la primera relación de ejercicios sobre programación funcional en Isabelle/HOL.
La teoría con las soluciones de los ejercicios es la siguiente
Read More “RA2017: Ejercicios de programación funcional con Isabelle/HOL”