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

[Randall R Schulz]

On Friday 12 October 2007 08:41, John F. Sowa wrote:
> Randall,
>
> 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.


> ...
>
> John


Randall Schulz