Abstract
ACL2 is a first-order, essentially quantifier free logic of computable recursive functions based on an applicative subset of Common Lisp. It supports lists as a primitive data structure. We describe how we have formalized a practical finite set theory for ACL2. Our finite set theory “book” includes set equality, set membership, the subset relation, set manipulation functions such as union, intersection, etc., a choice function, a representation of finite functions as sets of ordered pairs and a collection of useful functions for manipulating them (e.g., domain, range, apply) and others. The book provides many lemmas about these primitives, as well as macros for dealing with set comprehension and some other “higher order” features of set theory, and various strategies or tactics for proving theorems in set theory. The goal of this work is not to provide “heavy duty set theory” - a task more suited to other logics - but to allow the ACL2 user to use sets in a “light weight” fashion in specifications, while continuing to exploit ACL2’s efficient executability, built in proof techniques for certain domains, and extensive lemma libraries.
This work was supported in part by Compaq Systems Research Center, Palo Alto, CA.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Grzegorz Bancerek. A model of ZF set theory language. Journal of Formalized Mathematics, 1, 1989. http://mizar.org/JFM/Vol1/zf_lang.html.
M. J. C. Gordon. Higher order logic, set theory or both? In http://www.cl.cam.ac.uk/~mjcg/papers/holst/index.html. Invited talk, TPHOLs 96, Turku, Finland, August 1996.
M. Kaufmann, P. Manolios, and J S. Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, 2000.
M. Kaufmann, P. Manolios, and J S. Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Press, 2000.
M. Kaufmann and J S. Moore. Structured theory development for a mechanized logic. Journal of Automated Reasoning, 26(2):161–203, 2001.
L. Lamport. The temporal logic of actions. ACM Trans. on Programming Languages and Systems, 16(3):872–923, May 1994.
J S. Moore. Recursion by choose. In http://www.cs.utexas.edu/users/moore/publications/finite-set-theory/recursion-by-choose.lisp. Department of Computer Sciences, University of Texas at Austin, 2000.
Carlos Pacheco. Reasoning about TLA actions. Technical Report CS-TR-01-16, Computer Sciences, University of Texas at Austin, May 2001. http://www.cs.utexas.edu/ftp/pub/techreports/tr01-16.ps.Z.
L. C. Paulson. Set theory for verification: I. from foundations to functions. Journal of Automated Reasoning, 11:353–389, 1993.
L. C. Paulson. Set theory for verification: Ii. induction and recursion. Journal of Automated Reasoning, 15:167–215, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Moore, J.S. (2001). Finite Set Theory in ACL2. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_22
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_22
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive