[CL] Clausal Reasoners and The Absence of Lexical Signifiers for Variables
Randall R Schulz
rschulz at sonic.net
Fri Oct 12 10:51:09 CDT 2007
On Friday 12 October 2007 08:41, John F. Sowa wrote:
> There is no reason why the internal formats for a theorem prover
> should be identical to the interchange format.
I was hardly suggesting that. In fact, I didn't mention the interchange
format at all. I referred to "CL," not "CLIF."
I daresay, it's barely meaningful and certainly not feasible to use a
textual format as the internal representation of formulas in mechanical
reasoning or inference software. In my mind, formulas are trees.
Interchange formats are text, and hence linear.
More information about the CL