A Hierarchy of mathematical structures in ACL2
Authors:
Abstract:
In this paper, we provide 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 which characterize an algebraic structure and the generation of generic theories about a concrete structure. 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 in this paper means a great profit, with respect to a from scratch approach, when we work with complex mathematical structures; for instance, the ones coming from Algebraic Topology.