		Search-engine friendly clone of the ACL2 documentation.

Term

Termify

the process of converting a clause to a term

The ACL2 prover represents its goals and subgoals as clauses, e.g., lists of terms treated as disjunctions. The individual elements of a clause are called literals. For example a goal printed as (IMPLIES (AND p q) r) is internally represented as the 3-literal clause ((NOT p) (NOT q) r). A clause containing just one literal is called a unit clause.

To termify a clause containing multiple literals, we convert the clause to a unit clause using IF to express the disjunction. For example, the 3-literal clause ((NOT p) (NOT q) r) is propositionally equivalent to the term (IF (NOT P) 'T (IF (NOT Q) 'T R)). By embedding that IF-term in a singleton list we obtain a unit clause equivalent to the original 3-literal clause.

Applying an induction scheme to a clause containing multiple literals can produce an exponential number of cases. This does not happen if the clause is a unit clause. So the ACL2 induction mechanism sometimes termifies its goal clause before applying the induction scheme to shift the case-analysis burden to the rest of the prover.