At its heart, GL works by manipulating Boolean expressions. There are
many ways to represent Boolean expressions. GL currently supports a hons-based

For any particular proof, you can choose which representation to use by picking one of the available proof modes. Each representation has strengths and weaknesses, and the choice of representation can significantly impact performance. We give some advice about choosing these modes in modes.

The GL user does not need to know how BDDs and AIGs are represented; in this
documentation we will just adopt a conventional syntax to describe Boolean
expressions, e.g.,

GL groups Boolean expressions into **symbolic objects**. Much like a
Boolean expression can be evaluated to obtain a Boolean value, a symbolic
object can be evaluated to produce an ACL2 object. There are several kinds of
symbolic objects, but numbers are a good start. GL represents symbolic, signed
integers as

(:g-integer . <lsb-bits>)

Where

p = (:g-integer true false A & B false)

Then

GL uses another kind of symbolic object to represent ACL2 Booleans. In particular,

(:g-boolean . <val>)

represents

(:g-boolean . ~(A & B))

is a symbolic object whose value is

GL has a few other kinds of symbolic objects that are also tagged with
keywords, such as *also*
considered to be a symbolic object, and just represents itself. Furthermore, a
cons of two symbolic objects represents the cons of the two objects they
represent. For instance,

(1 . (:g-boolean . A & B))

represents either

One last kind of symbolic object we will mention represents an if-then-else among other symbolic objects. Its syntax is:

(:g-ite <test> <then> . <else>)

where

(:g-ite (:g-boolean . A) (:g-integer B A false) . #\C)

represents either 2, 3, or the character

GL doesn't have a special symbolic object format for ACL2 objects other than
numbers and Booleans. But it is still possible to create symbolic objects that
take any finite range of values among ACL2 objects, by using a nesting of