dc.creator | Heras, Jónathan | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Pascual, Vico | es |
dc.date.accessioned | 2019-05-20T11:10:16Z | |
dc.date.available | 2019-05-20T11:10:16Z | |
dc.date.issued | 2015 | |
dc.identifier.citation | Heras, J., Martín Mateos, F.J. y Pascual, V. (2015). Modelling algebraic structures and morphisms in ACL2. Applicable Algebra in Engineering, Communication and Computing, 26 (3), 277-303. | |
dc.identifier.issn | 0938-1279 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86550 | |
dc.description.abstract | In this paper, we present how algebraic structures and morphisms
can be modelled in the ACL2 theorem prover. Namely, we provide a guide-
line to implement a set of tools that facilitates the formalisations related to
algebraic structures | as a result, an algebraic hierarchy ranging from se-
toids 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 bene ts 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. | es |
dc.description.sponsorship | Ministerio de Educación y Ciencia MTM2009-13842-C02-01 | es |
dc.description.sponsorship | European Commission FP7 STREP project ForMath n. 243847 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | Applicable Algebra in Engineering, Communication and Computing, 26 (3), 277-303. | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.subject | Mathematical structures | es |
dc.subject | ACL2 | es |
dc.subject | Algebraic hierarchy | es |
dc.subject | Proof engineering | es |
dc.subject | Computer Algebra systems | es |
dc.subject | Formal veri cation | es |
dc.title | Modelling algebraic structures and morphisms in ACL2 | es |
dc.type | info:eu-repo/semantics/article | es |
dcterms.identifier | https://ror.org/03yxnpp24 | |
dc.type.version | info:eu-repo/semantics/submittedVersion | es |
dc.rights.accessRights | info:eu-repo/semantics/openAccess | es |
dc.contributor.affiliation | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial | es |
dc.relation.projectID | MTM2009-13842-C02-01 | es |
dc.relation.projectID | 243847 (ForMath) | es |
dc.relation.publisherversion | https://link.springer.com/article/10.1007/s00200-015-0252-9 | es |
dc.identifier.doi | 10.1007/s00200-015-0252-9 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 28 | es |
dc.journaltitle | Applicable Algebra in Engineering, Communication and Computing | es |
dc.publication.volumen | 26 | es |
dc.publication.issue | 3 | es |
dc.publication.initialPage | 277 | es |
dc.publication.endPage | 303 | es |
dc.identifier.sisius | 20814382 | es |