Menu Close

Etiqueta: Reseña

Reseña: Computational logic: its origins and applications

Lawrence C. Paulson publicó en 1998 el artículo Computational logic: its origins and applications cuyo resumen es

Computational logic is the use of computers to establish facts in a logical formalism. Originating in nineteenth century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the ‘logic for computable functions (LCF) approach’ pioneered by Robin Milner, where proofs can be constructed interactively or with the help of users’ code (which does not compromise correctness). A refinement of LCF, called Isabelle, retains these advantages while providing flexibility in the choice of logical formalism and much stronger automation. The main application of these techniques has been to prove the correctness of hardware and software systems, but increasingly researchers have been applying them to mathematics itself.

y su contenido es

  1. Introduction.
  2. A brief history of formal logic.
  3. Mechanized logic: the LCF tradition.
  4. A new theorem-proving architecture: Isabelle.
  5. Formalizing mathematics.
  6. Obstacles to formalizing mathematics.
  7. The way forward.

Reseña: Windmills of the minds: an algorithm for Fermat’s two squares theorem

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de números titulado Windmills of the minds: an algorithm for Fermat’s two squares theorem.

Sus autor es Hing Lun Chan (de la Australian National University en Canberra, Australia).

Su resumen es

The two squares theorem of Fermat is a gem in number theory, with a spectacular one-sentence “proof from the Book“. Here is a formalisation of this proof, with an interpretation using windmill patterns. The theory behind involves involutions on a finite set, especially the parity of the number of fixed points in the involutions. Starting as an existence proof that is non-constructive, there is an ingenious way to turn it into a constructive one. This gives an algorithm to compute the two squares by iterating the two involutions alternatively from a known fixed point.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

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

Reseña: Formalizing ordinal partition relations using Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre combinatoria titulado Formalizing ordinal partition relations using Isabelle/HOL.

Sus autores son

Su resumen es

This is an overview of a formalization project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all m ∈ ℕ, ω^ω → (ω^ω,m). This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic.

El trabajo se ha publicado en Experimental Mathematics.

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

Reseña: A machine-checked direct proof of the Steiner-Lehmus theorem

Se ha publicado un artículo de razonamiento formalizado en Nuprl sobre geometría titulado A machine-checked direct proof of the Steiner-Lehmus theorem.

Su autora es Ariel Kellison (de Cornell University).

Su resumen es

A direct proof of the Steiner-Lehmus theorem has eluded geometers for over 170 years. The challenge has been that a proof is only considered direct if it does not rely on reductio ad absurdum. Thus, any proof that claims to be direct must show, going back to the axioms, that all of the auxiliary theorems used are also proved directly. In this paper, we give a proof of the Steiner-Lehmus theorem that is guaranteed to be direct. The evidence for this claim is derived from our methodology: we have formalized a constructive axiom set for Euclidean plane geometry in a proof assistant that implements a constructive logic and have built the proof of the Steiner-Lehmus theorem on this constructive foundation.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

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

Reseña: Completeness theorems for first-order logic analysed in constructive type theory

Se ha publicado un artículo de razonamiento formalizado en Coq sobre lógica titulado Completeness theorems for first-order logic analysed in constructive type theory.

Sus autores son

Su resumen es

We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics à la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov’s Principle and Weak König’s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.

El trabajo se ha presentado en el Logical Foundations of Computer Science (LFCS 2020) y publicado en el Journal of Logic and Computation.

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

Reseña: Formalising Lie algebras in Lean

Se ha publicado un artículo de razonamiento formalizado en Lean sobre álgebras de Lie titulado Formalising Lie algebras.

Su autor es Oliver Nash (Imperial College in London, U.K.).

Su resumen es

Lie algebras are an important class of algebras which arise throughout mathematics and physics. We report on the formalisation of Lie algebras in Lean’s Mathlib library. Although basic knowledge of Lie theory will benefit the reader, none is assumed; the intention is that the overall themes will be accessible even to readers unfamiliar with Lie theory.

Particular attention is paid to the construction of the classical and exceptional Lie algebras. Thanks to these constructions, it is possible to state the classification theorem for finite-dimensional semisimple Lie algebras over an algebraically closed field of characteristic zero.

In addition to the focus on Lie theory, we also aim to highlight the unity of Mathlib. To this end, we include examples of achievements made possible only by leaning on several branches of the library simultaneously.

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

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

Reseña: Proving tree algorithms for succinct data structures

Se ha publicado un artículo de razonamiento formalizado en Coq sobre algorítmica titulado Proving tree algorithms for succinct data structures.

Sus autores son

Su resumen es

Succinct data structures give space efficient representations of large amounts of data without sacrificing performance. In order to do that they rely on cleverly designed data representations and algorithms. We present here the formalization in Coq/SSReflect of two different succinct tree algorithms. One is the Level-Order Unary Degree Sequence (aka LOUDS), which encodes the structure of a tree in breadth first order as a sequence of bits, where access operations can be defined in terms of Rank and Select, which work in constant time for static bit sequences. The other represents dynamic bit sequences as binary red-black trees, where Rank and Select present a low logarithmic overhead compared to their static versions, and with efficient Insert and Delete. The two can be stacked to provide a dynamic representation of dictionaries for instance. While both representations are well-known, we believe this to be their first formalization and a needed step towards provably-safe implementations of big data.

El trabajo se ha presentado el 30 de agosto en el JSSST 2018 (The 35th Meeting of the Japan Society for Software Science and Technology).

El código de las correspondientes teorías se encuentra GitHub.

Reseña: Formal verification of a geometry algorithm (A quest for abstract views and symmetry in Coq proofs)

Se ha publicado un artículo de razonamiento formalizado en Coq sobre geometría titulado Formal verification of a geometry algorithm: A quest for abstract views and symmetry in Coq proofs.

Su autor es Yves Bertot (del grupo MARELLE del INRIA, Sophia Antipolis).

Su resumen es

This extended abstract is about an effort to build a formal description of a triangulation algorithm starting with a naive description of the algorithm where triangles, edges, and triangulations are simply given as sets and the most complex notions are those of boundary and separating edges. When performing proofs about this algorithm, questions of symmetry appear and this exposition attempts to give an account of how these symmetries can be handled. All this work relies on formal developments made with Coq and the mathematical components library.

El trabajo se presentará el 16 de octubre en el ICTAC 2018 (15th International Colloquium on Theoretical Aspects of Computing).

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

Reseña: “Concrete semantics” with Coq and CoqHammer

Se ha publicado un artículo de razonamiento formalizado en Coq titulado “Concrete semantics” with Coq and CoqHammer.

Sus autores son

Su resumen es

The “Concrete Semantics” book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of the book using the Coq proof assistant. In order to achieve a similar brevity of the formal text we extensively use CoqHammer, as well as Coq Ltac-level automation. We compare the formalization efficiency, compactness, and the readability of the proof scripts originating from a Coq re-formalization of two chapters from the book.

El trabajo se ha presentado el 15 de agosto en el CICM 2018 (11th Conference on Intelligent Computer Mathematics).

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

Hammer for Coq (automation for dependent type theory)

Se ha publicado un artículo sobre automatización del razonamiento titulado Hammer for Coq (automation for dependent type theory).

Sus autores son Łukasz Czajka (de la Universidad de Varsovia) y Cezary Kaliszyk (del Computational Logic group la Universidad de Innsbruck).

Su resumen es

Hammers provide most powerful general purpose automation for proof assistants based on HOL and set theory today. Despite the gaining popularity of the more advanced versions of type theory, such as those based on the Calculus of Inductive Constructions, the construction of hammers for such foundations has been hindered so far by the lack of translation and reconstruction components. In this paper, we present an architecture of a full hammer for dependent type theory together with its implementation for the Coq proof assistant. A key component of the hammer is a proposed translation from the Calculus of Inductive Constructions, with certain extensions introduced by Coq, to untyped first-order logic. The translation is “sufficiently” sound and complete to be of practical use for automated theorem provers. We also introduce a proof reconstruction mechanism based on an eauto-type algorithm combined with limited rewriting, congruence closure and some forward reasoning. The algorithm is able to re-prove in the Coq logic most of the theorems established by the ATPs. Together with machine-learning based selection of relevant premises this constitutes a full hammer system. The performance of the whole procedure is evaluated in a bootstrapping scenario emulating the development of the Coq standard library. For each theorem in the library only the previous theorems and proofs can be used. We show that 40.8% of the theorems can be proved in a push-button mode in about 40 s of real time on a 8-CPU system.

El trabajo se ha publicado en el Journal of Automated Reasoning.

El código de CoqHammer se encuentra en GitHub.