LMF2019: Desarrollo de teorías formalizadas con Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos se ha estudiado cómo desarrollar en Isabelle/HOL teorías axiomáticas usando entornos locales (“locales”) y clases de tipos (“class”). Se ha aplicado al desarrollo de las teorías de grupos y a las de órdenes. videoconferencia.

La clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte:

  • Segunda parte:

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2019: Desarrollo de teorías formalizadas con Isabelle/HOL”

Vídeos de las clases de razonamiento automático con Isabelle/HOL

LMF2019: Razonamiento sobre árboles y bosques en Isabelle/HOL

En la clase de hoy del curso de Lógica matemática y fundamentos 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 clase se ha dado mediante videoconferencia y los vídeos correspondientes son:

  • Primera parte: Razonamiento sobre árboles binarios

  • Segunda parte: Árboles y bosques: Recursión mutua e inducción

La teoría utilizada es la siguiente

LMF2019: 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 clase se ha dado mediante videoconferencia y el vídeo correspondiente es:

La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “LMF2019: Razonamiento por casos y por inducción en Isabelle/HOL”