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

RA2017: Razonamiento automático sobre programas en Isabelle/HOL

En la segunda parte de la clase de hoy del curso de Razonamiento automático se han comenzado el estudio de la demostración automática de propiedades de programas funcionales en Isabelle/HOL.

En primer lugar, se ha estudiado cómo se pueden demostrar manualmente propiedades de programas Haskell. Para ello, se han usado las [transparencias del tema 8][http://www.cs.us.es/~jalonso/cursos/i1m-16/temas/tema-8.pdf) 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:

Como tarea se propuso la resolución de los ejercicios de la 2ª relación.

LMF2017: Deducción natural proposicional con Isabelle/HOL

En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha continuado el estudio de la deducción natural en la lógica proposicional con Isabelle/HOL.

La teoría Isabelle correspondiente es