[CL] Clausal Reasoners and The Absence of Lexical Signifiers for Variables

[John F. Sowa]

Randall,

There is no reason why the internal formats for a theorem prover
should be identical to the interchange format.  It could use a
a convention similar to what I used for CGIF in Annex B:

  1. In the original mapping of CGIF to and from KIF, I marked
     any identifier that occurs with a quantifier by the prefix
     "*" and any bound reference to it by the prefix "?".

  2. To support the no-prefix style of CLIF, I merely scan the
     given text and insert the appropriate prefix "*" or "?".

  3. I treat any strings that never occur in a quantifier as
     names, which I leave unmarked.

John