[CL] Clausal Reasoners and The Absence of Lexical Signifiers for Variables
John F. Sowa
sowa at bestweb.net
Fri Oct 12 10:41:18 CDT 2007
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.
More information about the CL