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-03T08:58:22Z | |
dc.date.available | 2019-05-03T08:58:22Z | |
dc.date.issued | 2009 | |
dc.identifier.citation | Martín Mateos, F.J., Rubio, J. y Ruiz Reina, J.L. (2009). ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System. En CICM 2009: International Conference on Intelligent Computer Mathematics (106-121), Grand Bend, Canada: Springer. | |
dc.identifier.isbn | 978-3-642-02613-3 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86203 | |
dc.description.abstract | Kenzo is a Computer Algebra system devoted to Algebraic
Topology, and written in the Common Lisp programming language. It is
a descendant of a previous system called EAT (for Effective Algebraic
Topology). Kenzo shows a much better performance than EAT due,
among other reasons, to a smart encoding of degeneracy lists as integers.
In this paper, we give a complete automated proof of the correctness of
this encoding used in Kenzo. The proof is carried out using ACL2, a system
for proving properties of programs written in (a subset of) Common
Lisp. The most interesting idea, from a methodological point of view, is
our use of EAT to build a model on which the verification is carried out.
Thus, EAT, which is logically simpler but less efficient than Kenzo, acts
as a mathematical model and then Kenzo is formally verified against it. | es |
dc.description.sponsorship | Ministerio de Educación y Ciencia MTM2006-06513 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | CICM 2009: International Conference on Intelligent Computer Mathematics (2009), p 106-121 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | ACL2 Verification of Simplicial Degeneracy Programs in the Kenzo System | es |
dc.type | info:eu-repo/semantics/conferenceObject | es |
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 | MTM2006-06513 | es |
dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/978-3-642-02614-0_13 | es |
dc.identifier.doi | 10.1007/978-3-642-02614-0_13 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 16 | es |
dc.publication.initialPage | 106 | es |
dc.publication.endPage | 121 | es |
dc.eventtitle | CICM 2009: International Conference on Intelligent Computer Mathematics | es |
dc.eventinstitution | Grand Bend, Canada | es |
dc.relation.publicationplace | Berlin | es |
dc.identifier.sisius | 6526293 | es |