Modelling algebraic structures and morphisms in ACL2

  1. Heras, J. 1
  2. Martín-Mateos, F.J. 2
  3. Pascual, V. 1
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 Universidad de Sevilla
    info

    Universidad de Sevilla

    Sevilla, España

    ROR https://ror.org/03yxnpp24

Revista:
Applicable Algebra in Engineering, Communications and Computing

ISSN: 0938-1279

Año de publicación: 2015

Volumen: 26

Número: 3

Páginas: 277-303

Tipo: Artículo

beta Ver similares en nube de resultados
DOI: 10.1007/S00200-015-0252-9 SCOPUS: 2-s2.0-84929706573 WoS: WOS:000354882400003 GOOGLE SCHOLAR

Otras publicaciones en: Applicable Algebra in Engineering, Communications and Computing

Repositorio institucional: lock_openAcceso abierto Postprint lockAcceso abierto Editor

Resumen

In this paper, we present how algebraic structures and morphisms can be modelled in the ACL2 theorem prover. Namely, we illustrate a methodology for implementing a set of tools that facilitates the formalisations related to algebraic structures—as a result, an algebraic hierarchy ranging from setoids to vector spaces has been developed. The resultant tools can be used to simplify the development of generic theories about algebraic structures. In particular, the benefits of using the tools presented in this paper, compared to a from-scratch approach, are especially relevant when working with complex mathematical structures; for example, the structures employed in Algebraic Topology. This work shows that ACL2 can be a suitable tool for formalising algebraic concepts coming, for instance, from computer algebra systems.