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

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 *negation* of

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

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

A moment's reflection shows that because of the rule

(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

But this may make more sense if we consider the clauses on which the prover
operated. Here are the clauses for

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,

Recall that a clause represents the disjunction of its literals. Since the
last literal of

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.