Menu Close

Etiqueta: Reseña

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.

Reseña: Comparison of two theorem provers: Isabelle/HOL and Coq

Se ha publicado un artículo de demostración asistida por ordenador titulado Comparison of two theorem provers: Isabelle/HOL and Coq.

Sus autores son

Su resumen es

The need for formal definition of the very basis of mathematics arose in the last century. The scale and complexity of mathematics, along with discovered paradoxes, revealed the danger of accumulating errors across theories. Although, according to Gödel’s incompleteness theorems, it is not possible to construct a single formal system which will describe all phenomena in the world, being complete and consistent at the same time, it gave rise to rather practical areas of logic, such as the theory of automated theorem proving. This is a set of techniques used to verify mathematical statements mechanically using logical reasoning. Moreover, it can be used to solve complex engineering problems as well, for instance, to prove the security properties of a software system or an algorithm. This paper compares two widespread tools for automated theorem proving, Isabelle/HOL and Coq, with respect to expressiveness, limitations and usability. For this reason, it firstly gives a brief introduction to the bases of formal systems and automated deduction theory, their main problems and challenges, and then provides detailed comparison of most notable features of the selected theorem provers with support of illustrative proof examples.

Reseña: A formal proof of the computation of Hermite normal form in a general setting

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado REGULAR-MT: A formal proof of the computation of Hermite normal form in a general setting.

Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).

Su resumen es

In this work, we present a formal proof of an algorithm to compute the Hermite normal form of a matrix based on our existing framework for the formalisation, execution, and refinement of linear algebra algorithms in Isabelle/HOL. The Hermite normal form is a well-known canonical matrix analogue of reduced echelon form of matrices over fields, but involving matrices over more general rings, such as Bézout domains. We prove the correctness of this algorithm and formalise the uniqueness of the Hermite normal form of a matrix. The succinctness and clarity of the formalisation validate the usability of the framework.

El trabajo se presentará el 17 de septiembre en el AISC 2018 (13th International Conference on Artificial Intelligence and Symbolic Computation).

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

Reseña: Formalized linear algebra over elementary divisor rings in Coq

Se ha publicado un artículo de razonamiento formalizado en Coq sobre álgebra titulado Formalized linear algebra over elementary divisor rings in Coq.

Sus autores son

Su resumen es

This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support essential operations of linear algebra, the classification theorem of finitely presented modules over such rings and the uniqueness of the Smith normal form up to multiplication by units. We present formally verified algorithms computing this normal form on a variety of coefficient structures including Euclidean domains and constructive principal ideal domains. We also study different ways to extend Bézout domains in order to be able to compute the Smith normal form of matrices. The extensions we consider are: adequacy (i.e. the existence of a gdco operation), Krull dimension ≤1 and well-founded strict divisibility.

El trabajo se ha publicado en Logical Methods in Computer Science (Volume 12, Issue 2).

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

Reseña: Proving divide and conquer complexities in Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Proving divide and conquer complexities in Isabelle/HOL

Su autor es Manuel Eberl (de la Technische Universität München, Alemania).

Su resumen es

The Akra–Bazzi method, a generalisation of the well-known Master Theorem, is a useful tool for analysing the complexity of Divide & Conquer algorithms. This work describes a formalisation of the Akra–Bazzi method (as generalised by Leighton) in the interactive theorem prover Isabelle/HOL and the derivation of a generalised version of the Master Theorem from it. We also provide some automated proof methods that facilitate the application of this Master Theorem and allow mostly automatic verification of Θ-bounds for these Divide & Conquer recurrences. To our knowledge, this is the first formalisation of theorems for the analysis of such recurrences.

La versión final del trabajo se ha publicado en el Journal of Automated Reasoning.

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: A decision procedure for univariate real polynomials in Isabelle/HOL

Se ha publicado un artículo de razonamiento formalizado en Isabelle sobre álgebra titulado A decision procedure for univariate real polynomials in Isabelle/HOL.

Su autor es Manuel Eberl (de la Technische Universität München, Alemania).

Su resumen es

Sturm sequences are a method for computing the number of real roots of a univariate real polynomial inside a given interval efficiently. In this paper, this fact and a number of methods to construct Sturm sequences efficiently have been formalised with the interactive theorem prover Isabelle/HOL. Building upon this, an Isabelle/HOL proof method was then implemented to prove interesting statements about the number of real roots of a univariate real polynomial and related properties such as non-negativity and monotonicity.

El trabajo se ha presentado en la CPP 2015 (The 4th ACM-SIGPLAN Conference on Certified Programs and Proofs).

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: Relation-algebraic verification of Prim’s minimum spanning tree algorithm

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Relation-algebraic verification of Prim’s minimum spanning tree algorithm.

Su autor es Walter Guttmann (de la University of Canterbury, Nueva Zelanda).

Su resumen es

We formally prove the correctness of Prim’s algorithm for computing minimum spanning trees. We introduce new generalisations of relation algebras and Kleene algebras, in which most of the proof can be carried out. Only a small part needs additional operations, for which we introduce a new algebraic structure. We instantiate these algebras by matrices over extended reals, which model the weighted graphs used in the algorithm. Many existing results from relation algebras and Kleene algebras generalise from the relation model to the weighted-graph model with no or small changes. The overall structure of the proof uses Hoare logic. All results are formally verified in Isabelle/HOL heavily using its integrated automated theorem provers.

El trabajo se presentará el 24 de octubre en el ICTAC2016 (13th International Colloquium on Theoretical Aspects of Computing).

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