Quantification in Tail-recursive Function Definitions

S. Ray

In P. Manolios and M. Wilding, editors, Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006, volume 205 of ACM International Conference Proceeding Series, pages 95-98. ACM

© 2006 ACL2 Steering Committee 0-9788493-0-2/06/08.

Abstract

We investigate the logical issues behind axiomatizing equations that contain both recursive calls and quantifiers in ACL2. We identify a class of such equations, named extended tail-recursive equations, that can be uniformly introduced in the logic. We point out some potential benefits of this axiomatization, and discuss the logical impediments behind introducing more general quantified formulas.

Relevant files

Paper preprint (ps, pdf)
Slides for ACL2 2006 (ps, pdf)
Supporting materials: See the directory books/workshops/2006/ray/support/ in the current ACL2 distribution. (Note: You need the workshops tarball. See the instructions for installing ACL2 in the ACL2 homepage.)

BibTex

@Inproceedings{ray-quantification,
  author    = "S. Ray",
  title     = "{Quantification in Tail-recursive Function Definitions}",
  editor    = "P. Manolios and M. Wilding",
  booktitle = "{Proceedings of the $6$th International Workshop on the ACL2
                Theorem Prover and Its Applications (ACL2 2006)}",
  address   = "{Seattle, WA}",
  series    = "ACM International Conference Series",
  volume    = "205",
  month     = aug,
  pages     = "95-98",
  year      = 2006,
  publisher = "ACM"
}