Efficient execution in an automated reasoning environment

Greve, David A.; Kaufmann, Matt; Manolios, Panagiotis; Moore, J. Strother; Ray, Sandip; Ruiz Reina, José Luis; Sumners, Rob; Vroon, Daron; Wilding, Matthew

doi:10.1017/S0956796807006338

Artículo

dc.creator	Greve, David A.	es
dc.creator	Kaufmann, Matt	es
dc.creator	Manolios, Panagiotis	es
dc.creator	Moore, J. Strother	es
dc.creator	Ray, Sandip	es
dc.creator	Ruiz Reina, José Luis	es
dc.creator	Sumners, Rob	es
dc.creator	Vroon, Daron	es
dc.creator	Wilding, Matthew	es
dc.date.accessioned	2019-05-07T09:40:04Z
dc.date.available	2019-05-07T09:40:04Z
dc.date.issued	2008
dc.identifier.citation	Greve, D.A., Kaufmann, M., Manolios, P., Moore, J.S., Ray, S., Ruiz Reina, J.L.,...,Wilding, M. (2008). Efficient execution in an automated reasoning environment. Journal of Functional Programming, 18 (1), 15-46.
dc.identifier.issn	0956-7968	es
dc.identifier.uri	https://hdl.handle.net/11441/86252
dc.description.abstract	We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.	es
dc.description.sponsorship	Ministerio de Educación y Ciencia TIN2004–03884	es
dc.format	application/pdf	es
dc.language.iso	eng	es
dc.publisher	Cambridge University Press	es
dc.relation.ispartof	Journal of Functional Programming, 18 (1), 15-46.
dc.rights	Attribution-NonCommercial-NoDerivatives 4.0 Internacional	*
dc.rights.uri	http://creativecommons.org/licenses/by-nc-nd/4.0/	*
dc.title	Efficient execution in an automated reasoning environment	es
dc.type	info:eu-repo/semantics/article	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	TIN2004-03884	es
dc.relation.publisherversion	https://www.cambridge.org/core/journals/journal-of-functional-programming/article/efficient-execution-in-an-automated-reasoning-environment/CA24027BF9359A7B0DF2A06CCED49DEA	es
dc.identifier.doi	10.1017/S0956796807006338	es
dc.contributor.group	Universidad de Sevilla. TIC137: Lógica, Computación e Ingeniería del Conocimiento	es
idus.format.extent	32	es
dc.journaltitle	Journal of Functional Programming	es
dc.publication.volumen	18	es
dc.publication.issue	1	es
dc.publication.initialPage	15	es
dc.publication.endPage	46	es
dc.identifier.sisius	6632575	es

Ficheros	Tamaño	Formato	Ver	Descripción
Efficient execution in an automated ...	388.1Kb	[PDF]	Ver/Abrir

Este registro aparece en las siguientes colecciones

Artículos (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