Reseña: Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en PVS titulado Formally-verified decision procedures for univariate polynomial computation based on Sturm’s and Tarski’s theorems

Sus autores son Anthony Narkawicz, César Muñoz y Aaron M. Dutle (del Formal Methods group en el NASA Langley Research Center).

Su resumen es

Sturm’s theorem is a well-known result in real algebraic geometry that provides a function that computes the number of roots of a univariate polynomial in a semi-open interval, not counting multiplicity. A generalization of Sturm’s theorem is known as Tarski’s theorem, which provides a linear relationship between functions known as Tarski queries and cardinalities of certain sets. The linear system that results from this relationship is in fact invertible and can be used to explicitly count the number of roots of a univariate polynomial on a set defined by a system of polynomial relations. This paper presents a formalization of these results in the PVS theorem prover, including formal proofs of Sturm’s and Tarski’s theorems. These theorems are at the basis of two decision procedures, which are implemented as computable functions in PVS. The first, based on Sturm’s theorem, determines satisfiability of a single polynomial relation over an interval. The second, based on Tarski’s theorem, determines the satisfiability of a system of polynomial relations over the real line. The soundness and completeness properties of these decision procedures are formally verified in PVS. The procedures and their correctness properties enable the implementation of PVS strategies for automatically proving existential and universal statements on polynomial systems. Since the decision procedures are formally verified in PVS, the soundness of the strategies depends solely on the internal logic of PVS rather than on an external oracle.

El trabajo se publicará en el Journal of Automated Reasoning.

El código de las correspondientes teorías en PVS del teorema de Sturm se encuentra aquí y el del teorema de Tarski aquí.

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: Automated generation of machine verifiable and readable proofs: A case study of Tarski’s geometry

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado Automated generation of machine verifiable and readable proofs: A case study of Tarski’s geometry.

Sus autores son

Su resumen es

The power of state-of-the-art automated and interactive the-orem provers has reached the level at which a significant portion of non-trivial mathematical contents can be formalized almost fully automat-ically. In this paper we present our framework for the formalization of mathematical knowledge that can produce machine verifiable proofs (for different proof assistants) but also human-readable (nearly textbook-like) proofs. As a case study, we focus on one of the twentieth century classics – a book on Tarski’s geometry. We tried to automatically generate such proofs for the theorems from this book using resolution theorem provers and a coherent logic theorem prover. In the first experiment, we used only theorems from the book, in the second we used additional lemmas from the existing Coq formalization of the book, and in the third we used specific dependency lists from the Coq formalization for each theorem. The results show that 37% of the theorems from the book can be auto-matically proven (with readable and machine verifiable proofs generated) without any guidance, and with additional lemmas this percentage rises to 42%. These results give hope that the described framework and other forms of automation can significantly aid mathematicians in developing formal and informal mathematical knowledge.

El trabajo se ha publicado en Annals of Mathematics and Artificial Intelligence.

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