DAO2012: Razonamiento sobre programas con Isabelle

PorJosé A. Alonso

En la sesión de hoy del seminario Demostración asistida por ordenador (DAO2012) se ha presentado cómo se puede demostrar con Isabelle propiedades de programas.

En el tema 8 del curso de I1M vimos cómo se puede razonar sobre programas funcionales. Hoy hemos visto cómo Isabelle puede hacer automáticamente las demostraciones de dicho tema. Los métodos que hemos usado son

  • simplificación (con simp),
  • automático (con auto),
  • inducción sobre números naturales y listas (con induct),
  • inducción con variables libres (con arbitrary) y
  • inducción en varias variables (con induct rule).

La teoría correspondiente a la clase es T3_Razonamiento_sobre_programas.thy cuyo contenido se muestra a continuación
Read More “DAO2012: Razonamiento sobre programas con Isabelle”

I1M2012: Ejercicios de definiciones por recursión y comprensión en Haskell (5)

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado las soluciones de los ejercicios 6 a 8 de la 11ª relación en las que se presentan ejercicios con dos definiciones (una por recursión y otra por comprensión) y la comprobación de la equivalencia de las dos definiciones con QuickCheck.

Los ejercicios, y sus soluciones, se muestran a continuación:
Read More “I1M2012: Ejercicios de definiciones por recursión y comprensión en Haskell (5)”

LI2012: Formas normales de Skolem y cláusulas

PorJosé A. Alonso

En la clase de hoy del curso Lógica Informática se estudiado cómo se puede diseñar un procedimiento de forma que dada una fórmula F obtenga otra G que no tenga cuantificadores, que esté en forma normal conjuntiva y que sea equisatisfacible con F (es decir, que G es satisfacible precisamente si lo es F). Con dicho procedimiento se calcula la forma normal de Skolem. A partir de las formas se Skolem se obtienen las formas clausales.

Las transparencias de esta clase son las del tema 10
Read More “LI2012: Formas normales de Skolem y cláusulas”