RA2011: Demostraciones por inducción en Isabelle

En la primera parte de la clase de hoy del curso de Razonamiento automático se ha ampliado el estudio de las demostraciones por inducción en Isabelle. Se ha estudiados:

  • cómo a veces es necesario generalizar las propiedades para poderla demostrar por inducción y cuantificar universalmente las variables libres,
  • cómo definir funciones recursivas que no son primitivas recursivas y cómo demostrar propiedades de dichas funciones usando el esquema de inducción generado por su definición y
  • cómo definir y demostrar propiedades de funciones definidas por recursión cruzada.

La clase se ha basado en la siguiente teoría Isabelle
Read More “RA2011: Demostraciones por inducción en Isabelle”

RA2011: Patrones de inducción en Isabelle: casos, inducción y otros

En la clase de hoy del curso de Razonamiento automático se han presentado los principales patrones de inducción en Isabelle: en la primera parte se ha presentado los patrones de de mostración por casos y por inducción y en la segunda parte se han presentado otros patrones (eliminación de disyunción, negación, contradicción y equivalencias).

La primera parte de la clase se ha basado en la siguiente teoría Isabelle
Read More “RA2011: Patrones de inducción en Isabelle: casos, inducción y otros”