Reseña: Formalizing divisibility rules as a student case study

Se ha publicado un artículo de razonamiento formalizado en Mizar sobre aritmética titulado Formalizing divisibility rules as a student case study.

Su autor es Adam Naumowicz (de la Univ. de Białystok en Polonia).

Su resumen es

We would like to present some results of a student case study administered as a part of an interactive theorem proving elective course for computer science students. The students’ task was to prove in Mizar the divisibility rules for selected primes based on the decimal representation of natural numbers. The formalized proofs were quite elementary, so a project like this could be carried out by a group of students without particularly strong mathematical background. In this paper we give a short overview of definitions that had to be introduced for the case study and present the way the divisibility rules were eventually formulated by the students. After that we discuss an example of a more interesting proof case, i.e. the divisibility by 11 rule.

El trabajo se ha presentado en CICM 2015 (the 8th Conference on Intelligent Computer Mathematics).