Día: 28 noviembre 2019

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

• el razonamiento por casos booleanos,
• el razonamiento por casos booleanos sobre una variable,
• el razonamiento por casos sobre listas,
• el razonamiento por inducción sobre números naturales con patrones,
• el razonamiento sobre definiciones con existenciales,
• el uso de librerías auxiliares (como Parity) y
• el uso de otros métodos de demostración (como presburg).

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”