A Theory About First-Order Terms in ACL2

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

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	2021-03-16T09:01:45Z
dc.date.available	2021-03-16T09:01:45Z
dc.date.issued	2002
dc.identifier.citation	Ruiz Reina, J.L., Alonso Jiménez, J.A., Hidalgo Doblado, M.J. y Martín Mateos, F.J. (2002). A Theory About First-Order Terms in ACL2. En ACL2 2002: Third International Workshop on the ACL2 Theorem Prover and Its Applications Grenoble, France: University of Texas.
dc.identifier.uri	https://hdl.handle.net/11441/106119
dc.description.abstract	We describe the development in ACL2 of a library of results about first-order terms. In particular, we present the formalization of some of the main properties of the complete lattice of first-order terms with respect to the subsumption relation. As a byproduct, verified executable implementations are obtained for some basic operations on firstorder terms, including matching, renaming, unification and anti-unification. This work can be seen as a basis for further studies about the formal properties of automated reasoning and symbolic computation systems.	es
dc.description.sponsorship	Ministerio de Ciencia y Tecnología TIC2000-1368-CO3-02	es
dc.format	application/pdf	es
dc.format.extent	23	es
dc.language.iso	eng	es
dc.publisher	University of Texas	es
dc.relation.ispartof	ACL2 2002: Third International Workshop on the ACL2 Theorem Prover and Its Applications (2002).
dc.rights	Attribution-NonCommercial-NoDerivatives 4.0 Internacional	*
dc.rights.uri	http://creativecommons.org/licenses/by-nc-nd/4.0/	*
dc.title	A Theory About First-Order Terms in ACL2	es
dc.type	info:eu-repo/semantics/conferenceObject	es
dcterms.identifier	https://ror.org/03yxnpp24
dc.type.version	info:eu-repo/semantics/publishedVersion	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	TIC2000-1368-CO3-02	es
dc.relation.publisherversion	https://www.cs.utexas.edu/users/moore/acl2/workshop-2002/	es
dc.eventtitle	ACL2 2002: Third International Workshop on the ACL2 Theorem Prover and Its Applications	es
dc.eventinstitution	Grenoble, France	es
dc.relation.publicationplace	Austin, TX, USA	es
dc.contributor.funder	Ministerio de Ciencia Y Tecnología (MCYT). España	es

Ficheros	Tamaño	Formato	Ver	Descripción
A theory about first-order terms ...	244.9Kb	[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