Reseña: A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre metalógica titulado A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle.

Su autor es Lawrence C. Paulson (de la Univ. de Cambridge, Inglaterra).

Su resumen es

An Isabelle/HOL formalisation of Gödel’s two incompleteness theorems is presented. The work follows Swierczkowski’s detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical encodings of syntax eliminates the necessity to formalise elementary number theory within an embedded logical calculus. The Isabelle formalisation uses two separate treatments of variable binding: the nominal package is shown to scale to a development of this complexity, while de Bruijn indices turn out to be ideal for coding syntax. Critical details of the Isabelle proof are described, in particular gaps and errors found in the literature.

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

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

Reseña: A framework for verified depth-first algorithms

PorJosé A. Alonso

En el CPP 2015 Peter Lammich y René Neumann presentarán el trabajo A framework for verifying depth-first search algorithms que está basado en el de René Neumann titulado A framework for verified depth-first algorithms.

El resumen de este último es

We present a framework in Isabelle/HOL for formalizing variants of depth-first search. This framework allows to easily prove non-trivial properties of these variants. Moreover, verified code in several programming languages including Haskell, Scala and Standard ML can be generated. In this paper, we present an abstract formalization of depth-first search and demonstrate how it is refined to an efficiently executable version. Further we use the emptiness-problem of Büchi-automata known from model checking as the motivation to present three Nested DFS algorithms. They are formalized, verified and transformed into executable code using our framework.

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