dc.creator | Lambán Pardo, Laureano | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.creator | Rubio, Julio | es |
dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2019-05-07T08:12:37Z | |
dc.date.available | 2019-05-07T08:12:37Z | |
dc.date.issued | 2013 | |
dc.identifier.citation | Lambán Pardo, L., Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2013). Certified Symbolic Manipulation: Bivariate Simplicial Polynomials. En ISAAC'13: 38th International Symposium on Symbolic and Algebraic Computation (243-250), Boston, Maine, USA: ACM. | |
dc.identifier.isbn | 978-1-4503-2059-7 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86250 | |
dc.description.abstract | Certified symbolic manipulation is an emerging new field
where programs are accompanied by certificates that, suitably interpreted, ensure the correctness of the algorithms. In
this paper, we focus on algebraic algorithms implemented in
the proof assistant ACL2, which allows us to verify correctness in the same programming environment. The case study
is that of bivariate simplicial polynomials, a data structure
used to help the proof of properties in Simplicial Topology.
Simplicial polynomials can be computationally interpreted in
two ways. As symbolic expressions, they can be handled
algorithmically, increasing the automation in ACL2 proofs.
As representations of functional operators, they help proving
properties of categorical morphisms. As an application of this
second view, we present the definition in ACL2 of some
morphisms involved in the Eilenberg-Zilber reduction, a central part of the Kenzo computer algebra system. We have
proved the ACL2 implementations are correct and tested
that they get the same results as Kenzo does. | es |
dc.description.sponsorship | Ministerio de Ciencia e Innovación MTM2009-13842 | es |
dc.description.sponsorship | Unión Europea nr. 243847 (ForMath) | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | ACM | es |
dc.relation.ispartof | ISAAC'13: 38th International Symposium on Symbolic and Algebraic Computation (2013), p 243-250 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Certified Symbolic Manipulation: Bivariate Simplicial Polynomials | es |
dc.type | info:eu-repo/semantics/conferenceObject | 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://dl.acm.org/citation.cfm?id=2465515 | es |
dc.identifier.doi | 10.1145/2465506.2465515 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 8 | es |
dc.publication.initialPage | 243 | es |
dc.publication.endPage | 250 | es |
dc.eventtitle | ISAAC'13: 38th International Symposium on Symbolic and Algebraic Computation | es |
dc.eventinstitution | Boston, Maine, USA | es |
dc.relation.publicationplace | New York | es |