El curso Informática (de 1º de Grado en Matemáticas) comenzará el miércoles 26 de septiembre de 2018.
Las clases son los miércoles y viernes de 9:00 a 11:00 en el aula EC04.
La página con los materiales del curso se encuentra en https://www.cs.us.es/~jalonso/cursos/i1m-18. En dicha página hay enlaces a
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.
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.
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í.
Esta entrada es una recopilación de lecturas compartidas, durante agosto de 2018, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante agosto de 2018”