dc.creator | Lambán Pardo, Laureano | es |
dc.creator | Rubio, Julio | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2019-05-20T09:01:54Z | |
dc.date.available | 2019-05-20T09:01:54Z | |
dc.date.issued | 2013 | |
dc.identifier.citation | Lambán Pardo, L., Rubio, J., Martín Mateos, F.J. y Ruiz Reina, J.L. (2013). Verifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithm. Logic Journal of the IGPL, 22 (1), 39-65. | |
dc.identifier.issn | 1367-0751 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86519 | |
dc.description.abstract | The Eilenberg–Zilber algorithm is one of the central components of the computer algebra system called Kenzo, devoted to
computing in Algebraic Topology. In this article we report on a complete formal proof of the underlying Eilenberg–Zilber
theorem, using the ACL2 theorem prover. As our formalization is executable, we are able to compare the results of the
certified programme with those of Kenzo on some universal examples. Since the results coincide, the reliability of Kenzo is
reinforced. This is a new step in our long-term project towards certified programming for Algebraic Topology. | es |
dc.description.sponsorship | Ministerio de Ciencia e Innovación MTM2009-13842 | es |
dc.description.sponsorship | European Union’s 7th Framework Programme [243847] (ForMath). | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Oxford Academic | es |
dc.relation.ispartof | Logic Journal of the IGPL, 22 (1), 39-65. | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.subject | Formalisation of mathematics | es |
dc.subject | Computational algebraic topology | es |
dc.subject | Program verification | es |
dc.title | Verifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithm | 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 | es |
dc.relation.projectID | 243847 (ForMath) | es |
dc.relation.publisherversion | https://academic.oup.com/jigpal/article/22/1/39/639519 | es |
dc.identifier.doi | 10.1093/jigpal/jzt034 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 27 | es |
dc.journaltitle | Logic Journal of the IGPL | es |
dc.publication.volumen | 22 | es |
dc.publication.issue | 1 | es |
dc.publication.initialPage | 39 | es |
dc.publication.endPage | 65 | es |