RA2018: Razonamiento sobre árboles y bosques 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 “RA2018: Razonamiento sobre árboles y bosques en Isabelle/HOL”

RA2018: Razonamiento por casos y por inducción 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 “RA2018: Razonamiento por casos y por inducción en Isabelle/HOL”

RA2018: Razonamiento estructurado sobre programas con 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 “RA2018: Razonamiento estructurado sobre programas con Isabelle/HOL”

RA2018: Razonamiento automático sobre programas en Isabelle/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 1ª relación.

En la segunda parte, se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las transparencias del tema 8 del curso de Informática (de 1º del Grado en Matemática). Como lectura complementaria se recomienda el capítulo 13 del libro de G. Hutton Programming in Haskell.

A continuación se ha explicado cómo demostrar automáticamente las propiedades anteriores con Isabelle/HOL.

El enunciado de las propiedades es inmediato: basta escribir la palabra lemma y a continuación la propiedad entre comillas dobles; por ejemplo,

También se puede poner un nombre al lema, por ejemplo,

La demostración es la palabra by seguida por el método de demostración. Los métodos que hemos usado son

  • by simp: que es el método de simplificación por reescritura,
  • by (induct x) auto: que es por inducción en x (donde x es un número natural o una lista) y simplificación automática de ambos casos,
  • by (induct rule: fn.induct) auto: que es por inducción según la definición de la función fn y simplificación automática de todos los casos,
  • by (simp add: lema_auxiliar): que es el método de simplificación por reescritura añadiéndole a las reglas de reescritura la correspondiente al lema_auxiliar,

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2018: Razonamiento automático sobre programas en Isabelle/HOL”