Reseña: A formal proof of Sasaki-Murao algorithm

PorJosé A. Alonso

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.

Reseña: Computing persistent homology within Coq/SSReflect

PorJosé A. Alonso

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: Formalizing Frankl’s conjecture: FC-families

PorJosé A. Alonso

En las CICM 2012 (Conferences on Intelligent Computer Mathematics) se ha presentado un trabajo de razonamiento formalizado en Isabelle/HOL titulado Formalizing Frankl’s conjecture: FC-families.

Sus autores son Filip Marić, Miodrag Živković y Bojan Vučković (del grupo ARGO (Automated Reasoning GrOup) de la Universidad de Belgrado).

Su resumen es

The Frankl’s conjecture, formulated in 1979. and still open, states that in every family of sets closed for unions there is an element contained in at least half of the sets. FC-families are families for which it is proved that every union-closed family containing them satisfies the Frankl’s condition (e.g., in every union-closed family that contains a one- element set a, the element a is contained in at least half of the sets, so families of the form a are the simplest FC-families). FC-families play an important role in attacking the Frankl’s conjecture, since they enable significant search space pruning. We present a formalization of the computer assisted approach for proving that a family is an FC-family. Proof-by-computation paradigm is used and the proof assistant Isabelle/HOL is used both to check mathematical content, and to perform (verified) combinatorial searches on which the proofs rely. FC-families known in the literature are confirmed, and a new FC-family is discovered.

El código con la formalización en Isabelle/HOL se encuentra aquí.

Reseña: Formalization and verification of number theoretic algorithms using the Mizar proof checker

PorJosé A. Alonso

En el FCS’12 (The 2012 International Conference on Foundations of Computer Science) se presentó un trabajo de razonamiento formalizado en Mizar titulado Formalization and verification of number theoretic algorithms using the Mizar proof checker.

Sus autores son Hiroyuki Okazaki, Yoshiki Aoki y Yasunari Shidama (de la Shinshu University).

Su resumen es

In this paper, we introduce formalization of well-known number theoretic algorithms on the Mizar proof checking system. We formalized the Euclidean algorithm, the extended Euclidean algorithm and the algorithm computing the solution of the Chinese reminder theorem based on the source code of NZMATH which is a Python based number theory oriented calculation system. We prove the accuracy of our formalization using the Mizar proof checking system as a formal verification tool.

Reseña: A refinement-based approach to computational algebra in Coq

PorJosé A. Alonso

El lunes (13 de agosto de 2012) se presentó en el ITP 2012 (Interactive Theorem Proving) un trabajo de razonamiento formalizado en Coq titulado A refinement-based approach to computational algebra in Coq.

Sus autores son Maxime Dénès (del INRIA Sophia Antipolis, Francia) y Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).

El resumen del trabajo es

We describe a step-by-step approach to the implementation and formal verification of efficient algebraic algorithms. Formal specifications are expressed on rich data types which are suitable for deriving essential theoretical properties. These specifications are then refined to concrete implementations on more efficient data structures and linked to their abstract counterparts. We illustrate this methodology on key applications: matrix rank computation, Winograd’s fast matrix product, Karatsuba’s polynomial multiplication, and the gcd of multivariate polynomials.

El código de la formalización en Coq se encuentra aquí.

Este trabajo es parte del proyecto ForMath: Formalisation of Mathematics.