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/HOL sobre metalógica titulado A mechanised proof of Gödel’s incompleteness theorems using Nominal Isabelle.

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

A Isabelle/HOL formalisation of Gödel’s two incompleteness theorems is presented. Aspects of the development are described in detail, including two separate treatments of variable binding: the nominal package and de Bruijn indices. The work follows Świerczkowski’s a detailed proof, using hereditarily finite set theory.

The machine proofs are fairly readable, thanks to the structured Isar proof language, and concise at under 14,000 lines for both theorems. The paper presents highlights of the proof, commenting on the advantages and disadvantages of the nominal framework and HF set theory. The proof reported here closely follows a detailed exposition by Świerczkowski. His careful and detailed proofs were indispensable, but significant deviations proved to be necessary. For the first time, we have complete, formal proofs of both theorems. They take the form of structured Isar proof scripts that can be examined interactively.

The total proof length of 14000 lines comprises 5000 lines for the second theorem and 9000 lines for the first. (One could also include 3000 lines for HF set theory itself, but then we may as well also count the standard libraries of natural numbers.)

This project took approximately one year, in time left available after fulfilling a Professor’s usual teaching and administrative duties. The underlying set theory took only two weeks to formalise. The Gödel development up to the proof formalisation condition took another five months. From there to the first incompleteness theorem took a further two months, mostly devoted to proving single valued properties. Then the second incompleteness theorem took a further four months, including much time wasted due to misunderstanding this perplexing material.

Introducción a la demostración asistida por ordenador con Isabelle/HOL

PorJosé A. Alonso

En el libro Introducción a la demostración asistida por ordenador con Isabelle/HOL he recopilado los temas y relaciones de ejercicios del curso de Razonamiento automático (2012-13).

El curso es una introducción a la demostración asistida por ordenador con Isabelle/HOL y consta de tres niveles.

En el primer nivel se presenta la formalización de las demostraciones por deducción natural. La presentación se basa en la realizada en los cursos de Lógica informática (de 2º del Grado en Informática) y Lógica matemática y fundamentos (de 3º del Grado en Matemáticas), en concreto en los temas de deducción natural proposicional y de primer orden. En este nivel se incluye los 3 primeros temas y las 6 primeras relaciones de ejercicios.

En el segundo nivel se presenta la programación funcional en Isabelle/HOL y el razonamiento sobre programas. La presentación se basa en la introducción a la programación con Haskell realizada en los cursos de Informática (de 1º del Grado en Matemáticas) y Programación declarativa (de 3º del Grado en Informática), en concreto en el tema 8 (para el razonamiento sobre programas) y en los restantes 9 primeros temas (para la programación funcional). En este nivel se incluye los temas 4, 5 y 6 y las relaciones de ejercicios desde la 7 a la 21.

En el tercer nivel se presentan casos de estudios y extensiones de la lógica para trabajar con conjuntos, relaciones y funciones. En este nivel se incluyen los temas 7 y 8 y las relaciones de ejercicios 22 y 23.

Tanto los temas como las relaciones de ejercicios se presentan como teorías de Isabelle/HOL (versión Isabelle2013). Conforme se necesitan se va comentando los elementos del Isabelle/HOL.

De Isabelle2013 se dispone se dispone de versiones libres para Linux, Windows y Mac OS X. Para instalarlo basta seguir la guía de instalación.

Proving soundness of combinatorial Vickrey auctions and generating verified executable code

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Proving soundness of combinatorial Vickrey auctions and generating verified executable code.

Sus autores son

Su resumen es

Using mechanised reasoning we prove that combinatorial Vickrey auctions are soundly specified in that they associate a unique outcome (allocation and transfers) to any valid input (bids). Having done so, we auto-generate verified executable code from the formally defined auction. This removes a source of error in implementing the auction design. We intend to use formal methods to verify new auction designs. Here, our contribution is to introduce and demonstrate the use of formal methods for auction verification in the familiar setting of a well-known auction.

El trabajo se ha desarrollado como parte del proyecto ForMaRE (Formal Mathematical Reasoning in Economics).

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

Formalization of basic linear algebra

PorJosé A. Alonso

Se ha publicado una tesis de máster de razonamiento formalizado en Isabelle/HOL titulada Formalization of basic linear algebra.

Su autor es Bhavisha M. Talsania (de la California State University, San Marcos).

Su resumen es

This thesis discusses the formalization of basic results from linear algebra up to the following theorems, using the computer proof checker Isabelle:

  • Theorem 1 (Basis Size Theorem): Suppose that V is a finite dimensional vector space. Then any two bases have the same number of elements.
  • Theorem 2 (Basis Characterization Theorem): Suppose that V is a vector space of dimension n. Then any spanning set has at least n elements, and any spanning set with exactly n elements is a basis. In addition, any linearly independent set of vectors has at most n elements, and any set of linearly independent vectors with exactly n elements is a basis.
  • Theorem 3 (Rank-Nullity Theorem): Let L : V1 → V2 be a linear map between finite dimensional vector spaces. Then the nullity of L plus the rank of L equals the dimension of V1 : dim(V1 ) = rank(L) + null(L).

Chapter 1 provides a discussion of informal and formal proofs and an introduction to the thesis topic. Chapter 2 provides a brief overview of the proof assistant Isabelle and it’s layout and syntax. Chapter 3 to Chapter 13 go into detail of the formalized proofs done in Isabelle. In Chapter 14, we end with remarks and conclusion of the thesis.

The Königsberg bridge problem and the friendship theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado The Königsberg bridge problem and the friendship theorem.

Su autor es Wenda Li (de la Universidad de Cambridge).

El artículo se ha publicado el 17 de julio en el Archive of Formal Proofs.

Su resumen es

This development provides a formalization of undirected graphs and simple graphs, which are based on Benedikt Nordhoff and Peter Lammich’s simple formalization of labelled directed graphs in the archive. Then, with our formalization of graphs, we show both necessary and sufficient conditions for Eulerian trails and circuits as well as the fact that the Königsberg Bridge Problem does not have a solution. In addition, we show the Friendship Theorem in simple graphs.