RA2010: Ejercicios de razonamiento proposicional con Isabelle

PorJosé A. Alonso

La clase de hoy del curso de Razonamiento automático ha consistido en la formalización en Isabelle/Isar de demostraciones por deducción natural en lógica proposicional. Para ello se han formalizado todas las demostraciones del tema de deducción natural proposicional del curso de Lógica informática

Las formalizaciones realizadas en clase se encuentran en el siguiente documento
Read More “RA2010: Ejercicios de razonamiento proposicional con Isabelle”

Open project position at TUM: Computer-supported verification of automata constructions

PorJosé A. Alonso

El grupo Foundations of Software Reliability and Theoretical Computer Science de la Universidad Politécnica de Munich ha anunciado la oferta de una plaza de trabajo en Lógica Computacional: Open project position at TUM: Computer-supported verification of automata constructions

El objetivo del trabajo es la realización de una biblioteca formalmente verificada con Isabelle de algoritmos de verificación de modelos (en inglés, model checking). El proyecto se enfoca en la aproximación a la verificación de modelos basada en automata. Por tanto, para su realización se será necesario formalizar en Isabelle los conceptos habituales de la teoría de automata.

Los directores del proyecto son Javier Esparza, Tobias Nipkow y Jan-Georg Smaus.

RA2010: Isabelle como un lenguaje funcional

PorJosé A. Alonso

En la clase de hoy del curso de Razonamiento automático se ha visto cómo se puede en Isabelle/HOL

  • calcular con los números naturales, los números enteros y los booleanos,
  • definir funciones mediante composición, condicionales, casos e inducción,
  • demostrar propiedades mediante simplificación,
  • definir tipos de datos recursivos,
  • definir y modificar registros y
  • refutar propiedades con QuickCheck.

Read More “RA2010: Isabelle como un lenguaje funcional”