Reseña: Coq, a proof assistant based on higher-order intuitionistic type theory

PorJosé A. Alonso

La semana pasada Jean-Pierre Jouannaud hizo una presentación sobre razonamiento automático en el Instituto de estudios avanzados de la Universidad de Tsinghua: Coq, a proof assistant based on higher-order intuitionistic type theory.

En la presentación se incluyen comentarios sobre objetivos y logros del razonamiento formalizado, los fundamentos teóricos de los demostradores, la correspondencia de Curry-Horward, el cálculo de construcciones de Coq y su adecuación.

Reseña: Philosophy of mathematics and computer science

PorJosé A. Alonso

Kazimierz Trzęsicki (del Departamento de Lógica, Informática y Filosofía de la Ciencia de la Universidad de Białystok, Polonia) ha publicado el artículo Philosophy of mathematics and computer science.

El resumen del artículo es

It is well known fact that the foundation of modern computer science were laid by logicians. Logic is at the heart of computing. The development of contemporary logic and the problems of the foundations of mathematics were in close mutual interaction. We may ask why the concepts and theories developed out of philosophical motives before computers were even invented, prove so useful in the practice of computing. Three main programmes together with the constructivist approach are discussed and the impact on computer science is considered.

En el artículo comenta las aportaciones a la ciencia de la computación de las tres escuelas lógicas de los fundamentos de la matemática:

  • del logicismo (de Frege, Russell y Withehead) resalta el sintaxis de la lógica como primer lenguaje de programación, los tipos, el lamda cálculo, LISP, la programación funcional y la lógica combinatoria como lenguaje de programación.
  • del formalismo (de Hilbert) destaca la máquina de Turing (como medio para resolver los problemas de decibilidad), la teoría de la computación, la demostración automática y el razonamiento formalizado.
  • del intuicionismo (de Brouwer) y del constructivismo (de Markov y Bishop) destaca la visión de “fórmulas-como-tipos”, la extracción de programas a partir de las pruebas, la teoría costructiva de tipos de Martin-Löf, los sistema de demostración asistida (Automath, NuPRL, LEGO, Agda, Twelf y Coq) y las teorías desarrolladas con dichos sistemas.

Reseña: Formalization of propositional linear temporal logic in the Mizar system

PorJosé A. Alonso

Una línea de trabajo dentro del campo del razonamiento formalizado consiste en la formalización de la metalógica de distintos sistemas lógicos. En esta línea se inscribe el artículo Formalization of propositional linear temporal logic in the Mizar system.

Su autor es Mariusz Giero (University of Bialystok).

Su resumen es

The paper describes formalization of some issues of propositional linear temporal logic (PLTL). We discuss encountered problems and applied solutions. The formalization was carried out in the Mizar system. In comparison with other systems, Mizar is famous for its large repository of computer checked mathematical knowledge and also for its user-friendly knowledge representation and proof language.

Reseña: Implementation of Bourbaki’s Elements of Mathematics in Coq. Part Two: Ordered Sets, Cardinals, Integers

PorJosé A. Alonso

En una entrada anterior comentamos el proyecto de formalización del libro Elements of Mathematics: Theory of Sets de N. Bourbaki en Coq.

En dicha entrada comentamos el primer paso del proyecto consistente en la formalización de la teoría de conjuntos correspondiente al capítulo II del libro de Bourbaki (páginas 65-130).

La formalización del capítulo III (páginas 131-256) constituye el contenido del segundo paso. Dicha formalización ha sido publicada por José Grimm en el artículo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part Two; Ordered Sets, Cardinals, Integers. Su resumen es el siguiente

We believe that it is possible to put the whole work of Bourbaki into a computer. One of the objectives of the Gaia project concerns homological algebra (theory as well as algorithms); in a first step we want to implement all nine chapters of the book Algebra. But this requires a theory of sets (with axiom of choice, etc.) more powerful than what is provided by Ensembles; we have chosen the work of Carlos Simpson as basis. This reports lists and comments all definitions and theorems of the Chapter Ordered Sets, Cardinals, Integers”.

Version 3 is based on the Coq ssreflect library. It implements some properties on ordinal numbers. The code (including some exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia.

Reseña: Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets

PorJosé A. Alonso

Una de las tareas del razonamiento formalizado consiste en la formalización de textos matemáticos. Un ejemplo es el artículo Implementation of Bourbaki’s Elements of Mathematics in Coq: Part One, Theory of Sets.

El autor del artículo es José Grimm (del INRIA Sophia-Antipolis Méditerranée) y se ha publicado en el Journal of Formalized Reasoning.

El trabajo se enmarca en el proyecto GAIA (Geometry, Algebra, Informatics and Applications), cuyos objetivos son la formalización de las demostraciones del la HDR (Habilitation à diriger des recherches) de A. Quadrat, de las del libro Basic Homological Algebra (de M. Scott Osborne) y la demostración de la corrección de la implementación de estos teoremas como algoritmos en el sistema OreModules.

Dentro del proyecto GAIA, el contenido del artículo es el primer paso y, esencialmente consiste en la formalización en Coq de teoremas del libro Elements of Mathematics: Theory of Sets de N. Bourbaki. La formalización se basa en la realizada por Carlos Simpson y publicada en Set-theoretical mathematics in Coq.

El resumen del artículo es el siguiente

This paper presents a formalization of the first book of the series Elements of Mathematics” by Nicolas Bourbaki, using the Coq proof assistant.

It discusses formalization of mathematics, and explains in which sense a computer proof of a statement corresponds to a proof in the Bourbaki sense, given that the Coq quantifiers are not defined in terms of Hilbert’s epsilon function. The list of axioms and axiom schemes of Bourbaki is compared to the more usual Zermelo-Fraenkel theory, and to those proposed by Carlos Simpson, which form the basis of the Gaia software. Some basic constructions (union, intersection, product, function, equivalence and order relation) are described, as well as some properties; this corresponds to Sections 1 to 6 of Chapter II, and the first two sections of Chapter III. A commented proof of Zermelo’s theorem is also given. The code (including almost all exercises) is available on the Web, under http://www-sop.inria.fr/apics/gaia.