Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/s00200-015-0252-9 | Appl. Algebra Eng. Commun. Comput. |
Keywords | Field | DocType |
Mathematical structures,ACL2,Algebraic hierarchy,Proof engineering,Computer algebra systems,Formal verification | Algebraic modeling language,Discrete mathematics,Dimension of an algebraic variety,Combinatorics,Function field of an algebraic variety,Algebra,A¹ homotopy theory,Differential algebraic geometry,Real algebraic geometry,Algebraic geometry and analytic geometry,Mathematics,Algebraic operation | Journal |
Volume | Issue | ISSN |
26 | 3 | 0938-1279 |
Citations | PageRank | References |
3 | 0.43 | 33 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Jónathan Heras | 1 | 94 | 23.31 |
| Francisco-Jesús Martín-Mateos | 2 | 3 | 0.43 |
| Vico Pascual | 3 | 3 | 0.43 |