Mostrar el registro sencillo del ítem

Artículo

dc.creatorLambán Pardo, Laureanoes
dc.creatorRubio, Julioes
dc.creatorMartín Mateos, Francisco Jesúses
dc.creatorRuiz Reina, José Luises
dc.date.accessioned2019-05-20T09:01:54Z
dc.date.available2019-05-20T09:01:54Z
dc.date.issued2013
dc.identifier.citationLambá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.issn1367-0751es
dc.identifier.urihttps://hdl.handle.net/11441/86519
dc.description.abstractThe 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.sponsorshipMinisterio de Ciencia e Innovación MTM2009-13842es
dc.description.sponsorshipEuropean Union’s 7th Framework Programme [243847] (ForMath).es
dc.formatapplication/pdfes
dc.language.isoenges
dc.publisherOxford Academices
dc.relation.ispartofLogic Journal of the IGPL, 22 (1), 39-65.
dc.rightsAttribution-NonCommercial-NoDerivatives 4.0 Internacional*
dc.rights.urihttp://creativecommons.org/licenses/by-nc-nd/4.0/*
dc.subjectFormalisation of mathematicses
dc.subjectComputational algebraic topologyes
dc.subjectProgram verificationes
dc.titleVerifying the bridge between simplicial topology and algebra: the Eilenberg–Zilber algorithmes
dc.typeinfo:eu-repo/semantics/articlees
dcterms.identifierhttps://ror.org/03yxnpp24
dc.type.versioninfo:eu-repo/semantics/submittedVersiones
dc.rights.accessrightsinfo:eu-repo/semantics/openAccesses
dc.contributor.affiliationUniversidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificiales
dc.relation.projectIDMTM2009-13842es
dc.relation.projectID243847 (ForMath)es
dc.relation.publisherversionhttps://academic.oup.com/jigpal/article/22/1/39/639519es
dc.identifier.doi10.1093/jigpal/jzt034es
dc.contributor.groupUniversidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimientoes
idus.format.extent27es
dc.journaltitleLogic Journal of the IGPLes
dc.publication.volumen22es
dc.publication.issue1es
dc.publication.initialPage39es
dc.publication.endPage65es

FicherosTamañoFormatoVerDescripción
Verifying the bridge between ...460.8KbIcon   [PDF] Ver/Abrir  

Este registro aparece en las siguientes colecciones

Mostrar el registro sencillo del ítem

Attribution-NonCommercial-NoDerivatives 4.0 Internacional
Excepto si se señala otra cosa, la licencia del ítem se describe como: Attribution-NonCommercial-NoDerivatives 4.0 Internacional