RA2010: Funciones recursivas generales en Isabelle

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha estudiado cómo definir funciones recursivas generales en Isabelle y cómo demostrar por inducción propiedades sobre las mismas. En concreto, se ha estudiado:

  • cómo definir funciones recursivas que no son primitivas recursivas (por ejemplo, la función de Ackermann) usando fun,
  • cómo obtener el esquema de inducción correpondiente a las definiciones anteriores,
  • cómo demostrar propiedades de las funciones antereiores con el esquema de inducción correspondiente,
  • cómo definir tipos de datos recursivos cruzados,
  • cómo obtener el esquema de inducción correpondiente a las definiciones anteriores,
  • cómo definr funciones con recursión cruzada,
  • cómo demostrar propiedades por inducción cruzada.

En la clase se ha presentado el tema 5 (desde la página 43 a la 47).

El código correspondiente se encuentra en Cap_5.thy .

I1M2010: Un calculador de tautologías en Haskell como caso de estudio de tipos de datos definidos

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado una aplicación de la definición de tipos. Concretamente, se ha estudiado cómo definir el tipo de las fórmulas proposicionales y, trabajando con dicho tipo, construir un programa para determinar si una fórmula es una tautología.

Las transparencias usadas en la clase son las del tema 9 (páginas 25-33):
Read More “I1M2010: Un calculador de tautologías en Haskell como caso de estudio de tipos de datos definidos”

I1M2010: Definiciones de tipos de datos en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se ha estudiado la definición de nuevos tipos de datos y de funciones sobre dichos tipos. Concretamente, se ha estudiado

  • cómo definir tipos usando type,
  • cómo definir funciones con dominio o rango en tipos definidos usando type,
  • cómo definir tipos usando data,
  • cómo definir funciones con dominio o rango en tipos definidos usando data y
  • cómo definir tipos de datos recursivos (p.e. naturales, listas y árboles).

Las transparencias usadas en la clase son las del tema 9 (páginas 1-24):
Read More “I1M2010: Definiciones de tipos de datos en Haskell”

RA2010: Patrones de demostración y heurística de generalización en Isabelle

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se han presentado los patrones fundamentales de demostración en Isabelle. En concreto, se han estudiado las demostraciones por casos, con negaciones, por contradicción, con equivalencias. También se ha estudiado la heurística de generalización en las demostraciones por inducción.

Las transparencias usadas en clase son las páginas 35-39 del tema 4 y las páginas 40-43 del tema 5.

El código correspondiente se encuentra en Cap_4.thy y Cap_5.thy.