Autor: José A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado Verification of an LCF-style first-order prover with equality.

Sus autores son Alexander Birch Jensen, Anders Schlichtkrull y Jørgen Villadsen (del grupo Algorithms, logic and graphs en la Technical University of Denmark (DTU))

Su resumen es

We formalize in Isabelle/HOL the kernel of an LCF-style prover for first-order logic with equality from John Harrison’s Handbook of Practical Logic and Automated Reasoning. We prove the kernel sound and generate Standard ML code from the formalization. The generated code can then serve as a verified kernel. By doing this we also obtain verified components such as derived rules, a tableau prover, tactics, and a small declarative interactive theorem prover. We test that the kernel and the components give the same results as Harrison’s original on all the examples from his book. The formalization is 600 lines and is available online.

El trabajo se presentará en el Isabelle Workshop 2016.

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre probabilidad titulado A formally verified proof of the central limit theorem

Sus autores son

• Jeremy Avigad (de la Carnegie Mellon University),
• Johannes Hölzl (del grupo Logic and Verification de la TU München) y
• Luke Serafin (de la Carnegie Mellon University).

Su resumen es

We describe a proof of the Central Limit Theorem that has been formally verified in the Isabelle proof assistant. Our formalization builds upon and extends Isabelle’s libraries for analysis and measure-theoretic probability. The proof of the theorem uses characteristic functions, which are a kind of Fourier transform, to demonstrate that, under suitable hypotheses, sums of random variables converge weakly to the standard normal distribution. We also discuss the libraries and infrastructure that supported the formalization, and reflect on some of the lessons we have learned from the effort.

El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí dentro del desarrollo de la teoría de la probabilidad.

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Refinement based verification of imperative data structures

Su autor es Peter Lammich (de la Chair for Logic and Verification en la Univ. técnica de Munich).

Su resumen es

In this paper we present a stepwise refinement based top-down approach to verified imperative data structures. Our approach is modular in the sense that already verified data structures can be used for construction of more complex data structures. Moreover, our data structures can be used as building blocks for the verification of algorithms. Our tool chain supports refinement down to executable code in various programming languages, and is fully implemented in Isabelle/HOL, such that its trusted code base is only the inference kernel and the code generator of Isabelle/HOL.

As a case study, we verify an indexed heap data structure, and use it to generate an efficient verified implementation of Dijkstra’s algorithm.

El trabajo se ha presentado en el CPP 2016 (The 5th ACM SIGPLAN Conference on Certified Programs and Proofs).

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