A Beginner's Guide To Reasoning about Quantification in ACL2
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.