Formalizing Rewriting in the ACL2 Theorem Prover

Ruiz Reina, José Luis; Alonso Jiménez, José Antonio; Hidalgo Doblado, María José; Martín Mateos, Francisco Jesús

doi:10.1007/3-540-44990-6_7

Ponencia

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

Ficheros	Tamaño	Formato	Ver	Descripción
acl2-rewriting.pdf	187.4Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Ponencias (Ciencias de la Computación e Inteligencia Artificial)

Mostrar el registro sencillo del ítem

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