dc.creator | Ruiz Reina, José Luis | es |
dc.creator | Alonso Jiménez, José Antonio | es |
dc.creator | Hidalgo Doblado, María José | es |
dc.creator | Martín Mateos, Francisco Jesús | es |
dc.date.accessioned | 2019-05-13T10:05:08Z | |
dc.date.available | 2019-05-13T10:05:08Z | |
dc.date.issued | 2000 | |
dc.identifier.citation | Ruiz Reina, J.L., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Martín Mateos, F.J. (2000). Formalizing Rewriting in the ACL2 Theorem Prover. En AISC 2000: International Conference on Artificial Intelligence and Symbolic Computation (92-106), Madrid, España: Springer. | |
dc.identifier.isbn | 978-3-540-42071-2 | es |
dc.identifier.issn | 0302-9743 | es |
dc.identifier.uri | https://hdl.handle.net/11441/86285 | |
dc.description.abstract | We present an application of the ACL2 theorem prover to formalize and reason about rewrite systems theory. This can be seen as a first approach to apply formal methods, using ACL2, to the design of symbolic computation systems, since the notion of rewriting or simplification is ubiquitous in such systems. We concentrate here on formalization and representation aspects of abstract reduction and term rewriting systems, using the first-order, quantifier-free ACL2 logic based on Common Lisp. | es |
dc.description.sponsorship | Ministerio de Educación y Ciencia PB96-0098-C04-04 | es |
dc.description.sponsorship | Ministerio de Educación y Ciencia PB96-1345 | es |
dc.format | application/pdf | es |
dc.language.iso | eng | es |
dc.publisher | Springer | es |
dc.relation.ispartof | AISC 2000: International Conference on Artificial Intelligence and Symbolic Computation (2000), p 92-106 | |
dc.rights | Attribution-NonCommercial-NoDerivatives 4.0 Internacional | * |
dc.rights.uri | http://creativecommons.org/licenses/by-nc-nd/4.0/ | * |
dc.title | Formalizing Rewriting in the ACL2 Theorem Prover | 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 | PB96-0098-C04-04 | es |
dc.relation.projectID | PB96-1345 | es |
dc.relation.publisherversion | https://link.springer.com/chapter/10.1007/3-540-44990-6_7 | es |
dc.identifier.doi | 10.1007/3-540-44990-6_7 | es |
dc.contributor.group | Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento | es |
idus.format.extent | 14 | es |
dc.publication.initialPage | 92 | es |
dc.publication.endPage | 106 | es |
dc.eventtitle | AISC 2000: International Conference on Artificial Intelligence and Symbolic Computation | es |
dc.eventinstitution | Madrid, España | es |
dc.relation.publicationplace | Berlin | es |
dc.identifier.sisius | 6531952 | es |