The logic of ACL2 is based on Common Lisp.

Common Lisp is the standard list processing programming language. It is
documented in: Guy L. Steele, **Common Lisp The Language**, Digital Press, 12
Crosby Drive, Bedford, MA 01730, 1990. See also
http://www.cs.cmu.edu/Web/Groups/AI/html/cltl/cltl2.html.

ACL2 formalizes only a subset of Common Lisp. It includes such familiar Lisp
functions as `cons`

, `car`

and `cdr`

for creating and manipulating list
structures, various arithmetic primitives such as `+`

, `*`

, `expt`

and
`<=`

, and `intern`

and `symbol-name`

for creating and manipulating
symbols. Control primitives include `cond`

, `case`

and `if`

, as well
as function call, including recursion. New functions are defined with
`defun`

and macros with `defmacro`

. See programming for a list
of the Common Lisp primitives supported by ACL2.

ACL2 supports five of Common Lisp's datatypes:

* the precisely represented, unbounded numbers (integers, rationals, and the complex numbers with rational components, called the ``complex rationals'' here),

* the characters with ASCII codes between 0 and 255

* strings of such characters

* symbols (including packages)

* conses

ACL2 is a very small subset of full Common Lisp. ACL2 does not include the
Common Lisp Object System (CLOS), higher order functions, circular
structures, and other aspects of Common Lisp that are **non-applicative**.
Roughly speaking, a language is applicative if it follows the rules of
function application. For example, `f(x)`

must be equal to `f(x)`

, which
means, among other things, that the value of `f`

must not be affected by
``global variables'' and the object `x`

must not change over time.