Efficient Execution in an Automated Reasoning Environment

D. A. Greve, M. Kaufmann, P. Manolios, J S. Moore, S. Ray, J. L. Ruiz-Reina, R. Sumners, D. Vroon, and M. Wilding

Journal of Functional Programming, volume 18(1), January 2008, pages 15-46. Cambridge University Press.

© 2007 Cambridge University Press. Copyright Statement

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.

Relevant files

Paper (pdf, Online version from CUP)
Supporting materials: See the directory books/defexec/ in the current ACL2 distribution.

BibTex

@Article{greve-efficient,
  author    = "D. A. Greve and M. Kaufmann and P. Manolios and J S. Moore and S. Ray and J. L. Ruiz-Reina and R. Sumners and D. Vroon and M. Wilding",
  title     = "{Efficient Execution in an Automated Reasoning Environment}",
  journal   = "{Journal of Functional Programming}",
  volume    = "18",
  number    = "1",
  pages     = "15-46",
  publisher = "{Cambridge University Press}",
  month     = jan,
  year      = "2007"
}