RA2017: Razonamiento por casos y por inducción en Isabelle/HOL

PorJosé A. Alonso

En la segunda parte de 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 teoría con los ejemplos presentados en la clase es la siguiente:
Read More “RA2017: Razonamiento por casos y por inducción en Isabelle/HOL”

Towards abstract and executable multivariate polynomials in Isabelle

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra computacional titulado Towards abstract and executable multivariate polynomials in Isabelle.

Sus autores son

Su resumen es

This work in progress report envisions a library for multivariate polynomials developed jointly by experts from computer theorem proving (CTP) and computer algebra (CA). The urgency of verified algorithms has been recognised in the field of CA, but the cultural gap to CTP is considerable; CA users expect high usability and efficiency. This work collects the needs of CA experts and reports on the design of a proof-of-concept prototype in Isabelle/HOL. The CA requirements have not yet been fully settled, and its development is still at an early stage. The authors hope for lively discussions at the Isabelle Workshop.

El trabajo se presentará el próximo domingo en el Isabelle Workshop del Vienna Summer of Logic (VSL2014).

Formalizing probabilistic noninterference

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Formalizing probabilistic noninterference

Sus autores son Andrei Popescu, Johannes Hölzl y Tobias Nipkow (de la Universidad Técnica de Munich, Alemania).

Su resumen es

We present an Isabelle formalization of probabilistic noninterference for a multi-threaded language with uniform scheduling. Unlike in previous settings from the literature, here probabilistic behavior comes from both the scheduler and the individual threads, making the language more realistic and the mathematics more challenging. We study resumption-based and trace-based notions of probabilistic noninterference and their relationship, and also discuss compositionality w.r.t. the language constructs and type-system-like syntactic criteria. The formalization uses recent development in the Isabelle probability theory library.

El trabajo se presentará en el CPP 2013 (3rd International Conference on Certified Programs and Proofs).

El código de las correspondientes teorías en Isabelle se encuentra aquí.

Reseña: Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)

PorJosé A. Alonso

Se ha publicado un artículo sobre formalización en Isabelle/Isar titulado Reading an algebra textbook.

Su autor es Clemens Ballarin (de la Technische Universität München) y lo presentó en el CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen es

We report on a formalisation experiment where excerpts from an algebra textbook are compared to their translation into formal texts of the Isabelle/Isar prover, and where an attempt is made in the formal text to stick as closely as possible with the structure of the informal counterpart. The purpose of the exercise is to gain understanding on how adequately a modern algebra text can be represented using the module facilities of Isabelle. Our initial results are promising.

Reseña: Certified HLints with Isabelle/HOLCF-Prelude

PorJosé A. Alonso

Se ha publicado un trabajo de verificación formal con Isabelle sobre Haskell titulado Certified HLints with Isabelle/HOLCF-Prelude.

Sus autores son Joachim Breitner, Brian Huffman, Neil Mitchell y Christian Sternagel.

El trabajo se presentará en el HART 2013 ( 1st International Workshop on Haskell And Rewriting Techniques).

Su resumen es

We present the HOLCF-Prelude, a formalization of a large part of Haskell’s standard prelude in Isabelle/HOLCF. Applying this formalization to the hints suggested by HLint allows us to certify them formally.

El códido del HOLCF-Prelude se encuentra aquí.