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: Deriving a fast inverse of the generalized Cantor N-tupling bijection

PorJosé A. Alonso

La semana que viene (6 de septiembre) se presentará en el ICLP’12 (28th International Conference on Logic Programming) un trabajo sobre resolución lógica de problemas combinatorios titulado Deriving a fast inverse of the generalized Cantor N-tupling bijection.

Su autor es Paul Tarau (de la University of North Texas, Denton, Texas, USA).

Su resumen es

We attack an interesting open problem (an efficient algorithm to invert the generalized Cantor N-tupling bijection) and solve it through a sequence of equivalence preserving transformations of logic programs, that take advantage of unique strengths of this programming paradigm. An extension to set and multiset tuple encodings, as well as a simple application to a “fair-search” mechanism illustrate practical uses of our algorithms.

The code in the paper (a literate Prolog program, tested with SWI-Prolog and Lean Prolog) is available at http://logic.cse.unt.edu/tarau/research/2012/pcantor.pl.

Reseña: Logic + control: An example of program construction

PorJosé A. Alonso

Se ha publicado un trabajo sobre metodología de la programación en Prolog titulado Logic + control: An example of program construction.

Su autor es Wlodzimierz Drabent (de la Univ. de Linköping, Suecia).

El trabajo se presentará el 6 de Septiembre en el ICLP’12 (28th International Conference on Logic Programming).

Su resumen es

We present a Prolog program (the SAT solver of Howe and King) as a logic program with added control. The control consists of a selection rule (delays of Prolog) and pruning the search space. We construct the logic program together with proofs of its correctness and completeness, with respect to a formal specification. This is augmented by a proof of termination under any selection rule. Correctness and termination are inherited by the Prolog program, the change of selection rule preserves completeness. We prove that completeness is also preserved by one case of pruning; for the other an informal justification is presented.

For proving correctness we use a method, which should be well known but is often neglected. A contribution of this paper is a method for proving completeness. In particular we introduce a notion of semi-completeness, for which a local sufficient condition exists.

We compare the proof methods with declarative diagnosis (algorithmic debugging). We introduce a method of proving that a certain kind of pruning preserves completeness. We argue that the proof methods correspond to natural declarative thinking about programs, and that they can be used, formally or informally, in every-day programming.

Reseña: Coherent and strongly discrete rings in type theory

PorJosé A. Alonso

Se ha publicado un nuevo trabajo de formalización de las matemáticas en Coq titulado Coherent and strongly discrete rings in type theory.

Sus autores son Tierry Coquand, Anders Mörtberg y Vincent Siles (de la Univ. de Gotemburgo, Suecia).

El trabajo se presentará en el CPP 2012 (The Second International Conference on Certified Programs and Proofs) que comenzará el 13 de diciembre.

Su resumen es

We present a formalization of coherent and strongly discrete rings in type theory. This is a fundamental structure in constructive algebra that represents rings in which it is possible to solve linear systems of equations. These structures have been instantiated with Bézout domains (for instance \mathbb{Z} and k[x]) and Prüfer domains (generalization of Dedekind domains) so that we get certified algorithms solving systems of equations that are applicable on these general structures. This work can be seen as basis for developing a formalized library of linear algebra over rings.

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

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

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.