Artículo
Efficient execution in an automated reasoning environment
Autor/es | Greve, David A.
Kaufmann, Matt Manolios, Panagiotis Moore, J. Strother Ray, Sandip Ruiz Reina, José Luis Sumners, Rob Vroon, Daron Wilding, Matthew |
Departamento | Universidad de Sevilla. Departamento de Ciencias de la Computación e Inteligencia Artificial |
Fecha de publicación | 2008 |
Fecha de depósito | 2019-05-07 |
Publicado en |
|
Resumen | 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 ... 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. |
Identificador del proyecto | TIN2004-03884 |
Cita | 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. |
Ficheros | Tamaño | Formato | Ver | Descripción |
---|---|---|---|---|
Efficient execution in an automated ... | 388.1Kb | [PDF] | Ver/ | |