Description:
In this paper, we provide a methodology allowing one to deal with
mathematical structures in the ACL2 theorem prover. Namely, we cope with the
representation of mathematical structures, the certifiation that an object fullls
the axioms which characterize an algebraic structure and the generation of generic
instances of a concrete structure. As a by-product, an ACL2 algebraic hierarchy
has been obtained. Our framework has been tested with the definition of homol-
ogy 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.