Reseña: A hierarchy of mathematical structures in ACL2

Se ha publicado un artículo de razonamiento formalizado en ACL2 titulado A hierarchy of mathematical structures in ACL2.

Sus autores son Jónathan Heras, Francisco J. Martín y Vico Pascual.

Su resumen es

In this paper, we present a methodology which allows one to deal with mathematical structures in the ACL2 theorem prover. Namely, we cope with the representation of mathematical structures, the certification that an object fulfills the axioms characterizing an algebraic structure and the generation of generic theories about concrete structures. As a by-product, an ACL2 algebraic hierarchy has been obtained. Our framework has been tested with the definition of homology groups, an example coming from Homological Algebra which involves several notions related to Universal Algebra. The method presented here, when compared to a from-scratch approach, is preferred when working with complex mathematical structures; for instance, the ones coming from Algebraic Topology. The final aim of this work is the verification of Computer Algebra systems, a field where our hierarchy fits better than the ones developed in other systems.

El códico correspondiente a este trabajo se encuentra aquí.