Steps towards verified implementations of HOL Light

PorJosé A. Alonso

Una de la líneas de trabajo dentro de la automatización del razonamiento es la verificación de sistemas de razonamiento. En dicha línea se ha publicado un trabajo titulado Steps towards verified implementations of HOL Light.

Sus autores son

Su resumen es

This short paper describes our plans and progress towards construction of verified ML implementations of HOL Light: the first formally proved soundness result for an LCF-style prover. Building on Harrison’s formalisation of the HOL Light logic and our previous work on proof-producing synthesis of ML, we have produced verified implementations of each of HOL Light’s kernel functions. What remains is extending Harrison’s soundness proof and proving that ML’s module system provides the required abstraction for soundness of the kernel to relate to the entire theorem prover. The proofs described in this paper involve the HOL Light and HOL4 theorem provers and the OpenTheory toolchain.

El trabajo se presentó en el ITP 2013 (4th Conference on Interactive Theorem Proving).

Reseña: Formal mathematics on display: A wiki for Flyspeck

PorJosé A. Alonso

Se ha publicado un artículo sobre la gestión del conocimiento matemático titulado Formal mathematics on display: A wiki for Flyspeck.

Sus autores son Carst Tankink, Cezary Kaliszyk, Josef Urban y Herman Geuvers.

El trabajo se presentará en las CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen es

The Agora system is a prototype “Wiki for Formal Mathematics”, with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype Flyspeck Wiki as an instance of Agora for HOL Light formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales’s informal Flyspeck book, and the formal Flyspeck development.

The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.

Reseña: Formalization of real analysis: A survey of proof assistants and libraries

PorJosé A. Alonso

Se ha publicado un artículo sobre razonamiento formalizado titudado Formalization of real analysis: A survey of proof assistants and libraries.

Sus autores son Sylvie Boldo, Catherine Lelay y Guillaume Melquiond.

Su resumen es

In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability, and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the proof automations these systems provide for real analysis.

Reseña: The Boyer-Moore waterfall model revisited

PorJosé A. Alonso

Uno de los problemas fundamentales dentro del campo del razonamiento automático es la automatización de la inducción. El método fundamental para automatizar la inducción es el de la cascada presentado por Robert S. Boyer y J S. Moore en su libro A Computational Logic e integrado en sus sistemas Nqthm y ACL2.

En el trabajo The Boyer-Moore waterfall model revisited se presenta una implementación del modelo de Boyer-Moore en el sistema HOL Light.

Sus autores son Petros Papapanagiotou y Jacques Fleuriot (de la Universidad de Edimburgo).

Su resumen es

In this paper, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. We analyze the basic concepts and methodology underlying this 30-year-old model and implement a new, fully integrated tool in the theorem prover HOL Light that can be invoked as a tactic. We also describe several extensions and enhancements to the model. These include the integration of existing HOL Light proof procedures and the addition of state-of-the-art generalization techniques into the waterfall. Various features, such as proof feedback and heuristics dealing with non-termination, that are needed to make this automated tool useful within our interactive setting are also discussed. Finally, we present a thorough evaluation of the approach using a set of 150 theorems, and discuss the effectiveness of our additions and relevance of the model in light of our results.

El trabajo es una extensión de la Tesis de Máster de Petros Papapanagiotou titulada On the automation of inductive proofs in HOL
Light y sirve como lectura complementaria en el curso Automated Reasoning (2012-13) de la Universidad de Edimburgo. Las transparencias del correspondiente tema del curso son Inductive theorem proving.

ProofWiki y la verificación de las demostraciones matemáticas

PorJosé A. Alonso

ProofWiki es un compendio de demostraciones matemáticas escritas de manera colaborativa en una wiki. Su objetivo es colecionar y clasificar demostraciones de teoremas matemáticos.

El proyecto empezó en marzo de 2008 y actualmente incluye 2.804 demostraciones escritas por sus 297 usuarios. Las demostraciones se encuentran clasificadas en 34 categorías. Una de las categorías particularmente interesante es la de teoremas con nombres en la que aparecen 247 teoremas. También es interesante la página de los teoremas más populares según el número de visitas.

ProofWiki podría servir de base para otro proyecto cuyo objetivo final fuese la verificación formal de las demostraciones matemáticas. Para ello se podría crear una wiki y, de forma colaborativa, escribir las verificaciones de las demostraciones de ProofWiki usando los distintos sistemas de razonamiento asistido por ordenador (como Isabelle/HOL/Isar, PVS, ACL2, Coq, HOL, HOL Light o Mizar).