Repositorio de producción científica de la Universidad de Sevilla

Efficient execution in an automated reasoning environment

 

Advanced Search
 
Opened Access Efficient execution in an automated reasoning environment
Cites

Show item statistics
Icon
Export to
Author: Greve, David A.
Kaufmann, Matt
Manolios, Panagiotis
Moore, J. Strother
Ray, Sandip
Ruiz Reina, José Luis
Sumners, Rob
Vroon, Daron
Wilding, Matthew
Department: Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial
Date: 2008
Published in: Journal of Functional Programming, 18 (1), 15-46.
Document type: Article
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.
Cite: 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.
Size: 388.1Kb
Format: PDF

URI: https://hdl.handle.net/11441/86252

DOI: 10.1017/S0956796807006338

See editor´s version

This work is under a Creative Commons License: 
Attribution-NonCommercial-NoDerivatives 4.0 Internacional

This item appears in the following Collection(s)