		Search-engine friendly clone of the ACL2 documentation.

Miscellaneous

Clause

A representation of prover goals

In ACL2, a clause is a list of terms, and the meaning of a clause is the ACL2 disjunction of those terms where a term p is considered ``false'' if ``p = nil'' and is true otherwise. The elements of a clause are called ``literals,'' even though they are just terms. For example the goal (IMPLIES (AND p q) r) is internally represented as the clause ((NOT p) (NOT q) r). The literals of that clause are the terms (NOT p), (NOT q), and r.

The ACL2 prover acts on clauses: a goal is represented as a clause, and each of the resulting subgoals is represented as a clause. Thus, the terms (literals) in a clause are all translated (see term).

To be precise, suppose that (L1 .. Lk M) is a clause containing at least two literals. ACL2 proof output displays that clause as an implication; this is called “prettyifying a clause”. Below, ~Li denotes the negation of Li in the following sense: if Li is of the form (NOT P) then ~Li designates P, and otherwise ~Li designates (NOT Li).

Prettyifying a clause with at least two literals
(L1 .. Lk M)
transforms it to the term
(IMPLIES (AND ~L1 ~L2 ... ~Lk)
         M).

Of course, the disjunction represented by the clause is propositionally equivalent to the resulting call of IMPLIES.

It is sometimes helpful to understand that ACL2's proof processes all operate on clauses. In particular, proof output — obtained when gag-mode is turned off or when using :pso or related utilities — may include a parenthetical remark as follows. WARNING: This parenthetical remark is printed only by the main simplifier, not by the preprocessor (see simple).

This simplifies (dropping false conclusion; see :DOC clause), using ....

What this remark signifies is that the last literal of the clause is false in at least one subgoal, and therefore does not appear in it (even in rewritten form). Let's see how that works with the following example.

(defstub foo (x) t)
(defaxiom foo-consp (implies (consp x) (foo x)))
(set-gag-mode nil)
(thm (implies (and (consp x) (natp (car x))) (not (foo x))))

The proof attempt starts as follows.

ACL2 !>(thm (implies (and (consp x) (natp (car x))) (not (foo x))))

By the simple :definition NATP we reduce the conjecture to

Goal'
(IMPLIES (AND (CONSP X)
              (INTEGERP (CAR X))
              (<= 0 (CAR X)))
         (NOT (FOO X))).

This simplifies (dropping false conclusion; see :DOC clause), using
the :rewrite rule FOO-CONSP, to

Goal''
(IMPLIES (AND (CONSP X) (INTEGERP (CAR X)))
         (< (CAR X) 0)).

The change from Goal' to Goal'' may be jarring because the “conclusion” — the second argument of the displayed IMPLIES call — has changed drastically. Let's analyze this change from the perspective of the goals printed; then we'll look at it from the perspective of clauses.

A moment's reflection shows that because of the rule FOO-CONSP, Goal' is equivalent to

(IMPLIES (AND (CONSP X)
              (INTEGERP (CAR X))
              (<= 0 (CAR X)))
         NIL).

And a little more reflection shows that the term above is propositionally equivalent to Goal'' above.

But this may make more sense if we consider the clauses on which the prover operated. Here are the clauses for Goal' and Goal''; the corresponding IMPLIES terms displayed above are obtained by prettyifying the respective clauses (in the sense of “prettyifying” discussed above).

Goal'
((NOT (CONSP X))
 (NOT (INTEGERP (CAR X)))
 (< (CAR X) '0)
 (NOT (FOO X)))

Goal''
((NOT (CONSP X))
 (NOT (INTEGERP (CAR X)))
 (< (CAR X) '0))

For each of these clauses, the third literal, (< (CAR X) '0), is just the negation of the (untranslated) term, (<= 0 (CAR X)), shown in the prover output.

Recall that a clause represents the disjunction of its literals. Since the last literal of Goal', (NOT (FOO X)), rewrote to NIL using the rule FOO-CONSP, it was dropped when creating Goal'': after all, (OR P NIL) is propositionally equivalent to P. So in Goal'' the last literal is (< (CAR X) '0). Therefore, the conclusion of each IMPLIES term obtained by prettyifying the clause has changed from (NOT (FOO X)) to (< (CAR X) '0).

Finally, note that although “dropping false conclusion” signifies that the conclusion was dropped in at least one subgoal, if however there are at least two subgoals then it might not be dropped in all of them. Consider the following variant of the earlier example.

(defstub foo (x) t)
(defaxiom foo-consp (implies (consp x) (foo x)))
(set-gag-mode nil)
(defstub bar (x) t)
; The proof fails for the following event (not important here).
(thm (implies (and (or (bar x) (consp x)) (natp (car x)))
              (not (foo x)))
     :otf-flg t)

The output includes the following.

Goal'
(IMPLIES (AND (OR (BAR X) (CONSP X))
              (INTEGERP (CAR X))
              (<= 0 (CAR X)))
         (NOT (FOO X))).

This simplifies (dropping false conclusion; see :DOC clause), using
the :rewrite rule FOO-CONSP, to the following two conjectures.

Subgoal 2
(IMPLIES (AND (BAR X)
              (INTEGERP (CAR X))
              (<= 0 (CAR X)))
         (NOT (FOO X))).

[[.. output elided ..]]

Subgoal 1
(IMPLIES (AND (CONSP X) (INTEGERP (CAR X)))
         (< (CAR X) 0)).

We see that the conclusion was false, hence dropped, in Subgoal 1, but remained in Subgoal 2.