Reseña: Reading an algebra textbook (by translating it to a formal document in the Isabelle/Isar language)

Se ha publicado un artículo sobre formalización en Isabelle/Isar titulado Reading an algebra textbook.

Su autor es Clemens Ballarin (de la Technische Universität München) y lo presentó en el CICM 2013 (Conferences on Intelligent Computer Mathematics).

Su resumen es

We report on a formalisation experiment where excerpts from an algebra textbook are compared to their translation into formal texts of the Isabelle/Isar prover, and where an attempt is made in the formal text to stick as closely as possible with the structure of the informal counterpart. The purpose of the exercise is to gain understanding on how adequately a modern algebra text can be represented using the module facilities of Isabelle. Our initial results are promising.