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: A Haskell library for term rewriting

PorJosé A. Alonso

Se ha publicado un artículo de automatización del razonamiento en Haskell titulado A Haskell library for term rewriting.

Sus autores son Bertram Felgenhauer, Martin Avanzini y Christian Sternagel.

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

Su resumen es

We present a Haskell library for first-order term rewriting covering basic operations on positions, terms, contexts, substitutions and rewrite rules. This effort is motivated by the increasing number of term rewriting tools that are written in Haskell.

La página de la librería se encuentra aquí.

Reseña: Theorem of three circles in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría algebraica titulado Theorem of three circles in Coq.

Su autora es Julianna Zsidó (de INRIA Sophia Antipolis).

Su resumen es

The theorem of three circles in real algebraic geometry guarantees the termination and correctness of an algorithm of isolating real roots of a univariate polynomial. The main idea of its proof is to consider polynomials whose roots belong to a certain area of the complex plane delimited by straight lines. After applying a transformation involving inversion this area is mapped to an area delimited by circles. We provide a formalisation of this rather geometric proof in Ssreflect, an extension of the proof assistant Coq, providing versatile algebraic tools. They allow us to formalise the proof from an algebraic point of view.

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í.