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

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.