Reseña: A formal proof of the Kepler conjecture

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL Light e Isabelle/HOL titulado A formal proof of the Kepler conjecture

Sus autores son Thomas Hales, Mark Adams, Gertrud Bauer, Dat Tat Dang, John Harrison, Truong Le Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Thang Tat Nguyen, Truong Quang Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, An Hoai Thi Ta, Trung Nam Tran, Diep Thi Trieu, Josef Urban, Ky Khac Vu y Roland Zumkeller.

Su resumen es

This article describes a formal proof of the Kepler conjecture on dense sphere packings in a combination of the HOL Light and Isabelle proof assistants. This paper constitutes the official published account of the now completed Flyspeck project.

Reseña: Certified Kruskal’s tree theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Certified Kruskal’s tree theorem

Su autor es Christian Sternagel (del Computational Logic Research Group en la Univ. de Insbruck, Austria).

Su resumen es

This article presents the first formalization of Kurskal’s tree theorem in a proof assistant. The Isabelle/HOL development is along the lines of Nash-Williams’ original minimal bad sequence argument for proving the tree theorem. Along the way, proofs of Dickson’s lemma and Higman’s lemma, as well as some technical details of the formalization are discussed.

El trabajo se ha publicado en Journal of Formalized Reasoning.

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

I1M2014: El TAD (tipo abstracto de datos) de las tablas en Haskell

PorJosé A. Alonso

En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha estudiado cómo trabajar con tablas en Haskell usando el módulo Data.Array y en la segunda parte se ha estudiado el TAD (tipo abstracto de datos) de las tablas y tres implementaciones en Haskell: como funciones, como listas de asociación y como matrices.

Una tabla (array en inglés) es una colección de elementos (valores) a los que se accede mediante sus índices<.

El contenido la segunda parte ha sido el siguiente:

  • la signatura del TAD de las tablas;
  • las propiedades del TAD de las tablas;
  • las implementaciones, en Haskell, de las tablas mediante funciones, listas de asociación y matrices y
  • la comprobación con QuickCheck de sus propiedades.

Read More “I1M2014: El TAD (tipo abstracto de datos) de las tablas en Haskell”