En la clase de hoy del curso Lógica matemática y fundamentos se han resuelto los ejercicios 22, 27, 28, 29, 32 y 34 de la relación 7 sobre deducción natural en lógica de primer orden con Isabelle/HOL.
Las soluciones de los ejercicios resueltos se muestran a continuación:
Read More “LMF2013: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (2)”
Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado A fully verified executable LTL model checker.
Sus autores son Javier Esparza, Peter Lammich, René Neumann, Tobias Nipkow, Alexander Schimpf y Jan-Georg Smaus.
El trabajo se presentará en el CAV 2013 (25th International Conference on Computer Aided Verification).
Su resumen es
We present an LTL model checker whose code has been completely verified using the Isabelle theorem prover. The checker consists of over 4000 lines of ML code. The code is produced using recent Isabelle technology called the Refinement Framework, which allows us to split its correctness proof into (1) the proof of an abstract version of the checker, consisting of a few hundred lines of “formalized pseudocode”, and (2) a verified refinement step in which mathematical sets and other abstract structures are replaced by implementations of efficient structures like red-black trees and functional arrays. This leads to a checker that, while still slower than unverified checkers, can already be used as a trusted reference implementation against which advanced implementations can be tested. We report on the structure of the checker, the development process, and some experiments on standard benchmarks.
El trabajo forma parte del proyecto CAVA (Computer Aided Verification of Automata).
El código de las correspondientes teorías Isabelle/HOL se encuentra aquí.
En la segunda parte de la clase de hoy del curso de Razonamiento automático se ha presentado cómo se puede demostrar propiedades de programas funcionales con Isabelle/HOL.
En la presentación se han usado los ejemplos del tema 8 del curso de Informática (de 1º del Grado en Matemáticas).
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Razonamiento sobre programas con Isabelle/HOL (1)”
En la primera parte de la clase de hoy del curso de Razonamiento automático se ha presentado la programación funcional en Isabelle/HOL.
La teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2012: Programación funcional con Isabelle/HOL”
En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han resueltolos 5 primeros ejercicios de la relación 24. El objetivo de esta relación es ampliar el conjunto de operaciones
sobre polinomios definidas utilizando las implementaciones del TAD de
polinomio estudiadas en el tema 21. Además, en algunos ejemplos de usan polinomios con coeficientes racionales. En Haskell, el número racional x/y se representa por x%y. El TAD de los números racionales está definido en el módulo Data.Ratio.
En los ejercicios se usan las siguientes librerías, estudiadas en el tema 21,
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Operaciones con el TAD de los polinomios en Haskell (1)”