A Beginner's Guide To Reasoning about Quantification in ACL2

S. Ray

Original Date: February 14, 2005.
Last Updated: November 9, 2008.

Incorporated in the ACL2 User's Manual, August 2008.


ACL2 is a first-order logic which permits reasoning about quantification through Skolemization. Many ACL2 users get stumped while starting to reason about quantifiers in ACL2. This tutorial is intended to provide guidance and advice to the beginning ACL2 user intending to use quantification with the theorem prover.

Relevant files