dc.creator | Ruiz Reina, José Luis | es |
dc.date.accessioned | 2019-05-15T10:57:15Z | |
dc.date.available | 2019-05-15T10:57:15Z | |
dc.date.issued | 2014 | |
dc.identifier.citation | Ruiz Reina, J.L. (2014). Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems. En AISC 2014: 12th International Conference on Artificial Intelligence and Symbolic Computation (1-6), Sevilla, España: Springer. | |
dc.identifier.isbn | 978-3-319-13769-8 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86390 | |
dc.description.abstract | The application of automated reasoning to the formal verification
of symbolic computation systems is motivated by the need of
ensuring the correctness of the results computed by the system, beyond
the classical approach of testing. Formal verification of properties of the
implemented algorithms require not only to formalize the properties of
the algorithm, but also of the underlying (usually rich) mathematical
theory.
We show how we can use ACL2, a first-order interactive theorem
prover, to reason about properties of algorithms that are typically implemented
as part of symbolic computation systems. We emphasize two
aspects. First, how we can override the apparent lack of expressiveness we
have using a first-order approach (at least compared to higher-order logics).
Second, how we can execute the algorithms (efficiently, if possible)
in the same setting where we formally reason about their correctness.
Three examples of formal verification of symbolic computation algorithms
are presented to illustrate the main issues one has to face in this
task: a Gr¨obner basis algorithm, a first-order unification algorithm based
on directed acyclic graphs, and the Eilenberg-Zilber algorithm, one of
the central components of a symbolic computation system in algebraic
topology. | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | AISC 2014: 12th International Conference on Artificial Intelligence and Symbolic Computation (2014), p 1-6 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Proving and Computing: Applying Automated Reasoning to the Verification of Symbolic Computation Systems | 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.publisherversion | https://link.springer.com/chapter/10.1007/978-3-319-13770-4_1 | es |
dc.identifier.doi | 10.1007/978-3-319-13770-4_1 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 6 | es |
dc.publication.initialPage | 1 | es |
dc.publication.endPage | 6 | es |
dc.eventtitle | AISC 2014: 12th International Conference on Artificial Intelligence and Symbolic Computation | es |
dc.eventinstitution | Sevilla, España | es |
dc.relation.publicationplace | Berlin | es |
dc.identifier.sisius | 20746868 | es |