I1M2012: Comienzo del curso
Las clases del curso Informática (de 1º de Grado en Matemáticas) comenzarán el lunes 1 de octubre.
Reseña: A formal proof of Sasaki-Murao algorithm
La semana pasada se presentó en el MAP2012 (Mathematics, Algorithms and Proofs 2012) un trabajo de aplicación de bibliotecas de razonamiento formalizado en Coq a la verificación de un algoritmo de álgebra computacional.
El título del trabajo es A formal proof of Sasaki-Murao algorithm y sus autores son Tierry Coquand, Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).
El resumen del trabajo es
The Sasaki-Murao algorithm computes the determinant of any square matrix over a commutative ring in polynomial time. The algorithm itself can be written as a short and simple functional program, but its correctness involves non-trivial mathematics. We here represent this algorithm in Type Theory with a new correctness proof, using the Coq proof assistant and the SSReflect extension.
El código Coq de la formalización se encuentra aquí y las transparencias de la presentación se encuentran aquí.
Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.
LI2012: Presentación del curso de “Lógica informática” (2012-13)
En la clase de hoy, se ha realizado la presentación del curso Lógica Informática siguiendo el plan de la asignatura. Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red:
- la página de la asignatura,
- las transparencias de los temas,
- el libro con los apuntes de los temas,
- el libro sobre la construcción lógica de sistemas lógicos,
- el libro con los enunciados de los ejercicios,
- el libro de exámenes resueltos de cursos anteriores
- el libro de ejercicios de formalización,
- el libro de soluciones de los ejercicios de deducción natural proposicional y
- el libro de soluciones de los ejercicios de deducción natural en lógica de primer orden.
- el libro con los apuntes de los temas,
Reseña: Computing persistent homology within Coq/SSReflect
Se ha publicado un nuevo trabajo de razonamiento formalizado en Coq titulado Computing persistent homology within Coq/SSReflect.
Sus autores son Jónathan Heras, Thierry Coquand, Anders Mörtbeg y Vincent Siles.
Su resumen es
Persistent homology is one of the most active branches of Computational Algebraic Topology with applications in several contexts such as optical character recognition or analysis of point cloud data. In this paper, we report on the formal development of certified programs to compute persistent Betti numbers, an instrumental tool of persistent homology, using the Coq proof assistant together with the SSReflect extension. To this aim it has been necessary to formalize the underlying mathematical theory of these algorithms. This is another example showing that interactive theorem provers have reached a point where they are mature enough to tackle the formalization of nontrivial mathematical theories.
Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.
Reseña: Improving real analysis in Coq: a user-friendly approach to integrals and derivatives
En la CPP 2012 (The Second International Conference on Certified Programs and Proofs), que comenzará el 13 de diciembre, se presentará un trabajo de verificación formal en Coq titulado Improving real analysis in Coq: a user-friendly approach to integrals and derivatives.
Sus autores son Sylvie Boldo, Catherine Lelay y Guillaume Melquiond (del grupo ProVal (Proof of Programs) en el INRIA Saclay – Île-de-France).
Su resumen es
Verification of numerical analysis programs requires dealing with derivatives and integrals. High confidence in this process can be achieved using a formal proof checker, such as Coq. Its standard library provides an axiomatization of real numbers and various lemmas about real analysis, which may be used for this purpose. Unfortunately, its definitions of derivative and integral are unpractical as they are partial functions that demand a proof term. This proof term makes the handling of mathematical formulas cumbersome and does not conform to traditional analysis. Other proof assistants usually do not suffer from this issue; for instance, they may rely on Hilbert’s epsilon to get total operators. In this paper, we propose a way to define total operators for derivative and integral without having to extend Coq’s standard axiomatization of real numbers. We proved the compatibility of our definitions with the standard library’s in order to leverage existing results. We also greatly improved automation for real analysis proofs that use Coq standard definitions. We exercised our approach on lemmas involving iterated partial derivatives and differentiation under the integral sign, that were missing from the formal proof of a numerical program solving the wave equation.
Este trabajo forma parte del proyecto Coquelicot.
El código con las teorías correspondiente se encuentra aquí.