Finite Set Theory in ACL2

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.

Note: This paper was accepted for The 14th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2001) and will appear in the associated LNCS volume.

Supporting Files

• paper (76 KB gzipped postscript)
• paper (114 KB gzipped pdf)
• books.tar (154 tar file): the source files for all the ACL2 books and the scripts needed to re-certify them.
• Source files in books.tar
  • Makefile: A Unix makefile that will re-certify all of the relevant books.
  • total-ordering.lisp: a book defining a total ordering on ACL2 objects, used in the canonicalization of sets.
  • defpkg.lisp: the definition of the "S" symbol package.
  • set-theory.lisp: the main set-theory book.
  • set-theory.acl2: the file that tells the Makefile how to certify set-theory.lisp.
  • powerset-examples.lisp
  • powerset-examples.acl2: the file that tells the Makefile how to certify powerset-examples.lisp.
  • set-count.lisp
  • set-count.acl2: the file that tells the Makefile how to certify set-count.lisp.
  • recursion-by-choose.lisp
  • recursion-by-choose.acl2: the file that tells the Makefile how to certify recursion-by-choose.lisp.