A precise description of the ACL2 logic

The ACL2 logic is a rst-order, essentially quantier-free logic of total re-cursive functions providing mathematical induction and several extension prin-ciples, including symbol package denition and recursive function denition. In this document we describe the logic more precisely.