CLAUSE-IDENTIFIER

Major Section:  MISCELLANEOUS

To each goal-spec, str, there corresponds a clause-identifier produced by (parse-clause-id str). For example,

(parse-clause-id "[2]Subgoal *4.5.6/7.8.9'''")

The function string-for-tilde-@-clause-id-phrase inverts parse-clause-id in the sense that given a clause identifier it returns the corresponding goal-spec.

As noted in the documentation for goal-spec, each clause printed in the theorem prover's proof attempt is identified by a name. When these names are represented as strings they are called ``goal specs.'' Such strings are used to specify where in the proof attempt a given hint is to be applied. The function parse-clause-id converts goal-specs into clause identifiers, which are cons-trees containing natural numbers.

Examples of goal-specs and their corresponding clause identifiers are shown below.

             parse-clause-id
                   -->

"Goal"                       ((0) NIL . 0)
"Subgoal 3.2.1'"             ((0) (3 2 1) . 1)
"[2]Subgoal *4.5.6/7.8.9'''" ((2 4 5 6) (7 8 9) . 3)

                   <--
      string-for-tilde-@-clause-id-phrase

The caar of a clause id specifies the forcing round, the cdar specifies the goal being proved by induction, the cadr specifies the particular subgoal, and the cddr is the number of primes in that subgoal.

Internally, the system maintains clause ids, not goal-specs. The system prints clause ids in the form shown by goal-specs. When a goal-spec is used in a hint, it is parsed (before the proof attempt begins) into a clause id. During the proof attempt, the system watches for the clause id and uses the corresponding hint when the id arises. (Because of the expense of creating and garbage collecting a lot of strings, this design is more efficient than the alternative.)