[ontoiop-forum] DOL finalisation

[John F Sowa]

Till,

Thanks for the clarifications.  For now, that covers all the issues
I was concerned about.

> A certain step towards prover cooperation is to speculate lemmas
> and then use a different theorem provers for the lemmas and
> the main theorem.

Yes.  That could probably support a hybrid where a general FOL
theorem prover has primary control, but it calls special-purpose
theorem provers to prove lemmas expressed in more restricted
subsets of FOL.  For example, is S1 a subsort of S2?

>> (= f (lambda (x y) ("some expression that uses x and y")))
>> 
>> This is a convenient notation in LISP and other languages,
> If you restrict this to first-order definitions, then it seems harmless
> to me (though I cannot see what is gained by this notation).

For defining a function, I agree that this syntax has no advantage over
(forall (x y) (= (f x y) ("some expression that uses x and y")))

But the lambda syntax is most useful when you want to use a function
without giving it a name -- for example, when it's an argument of
some other function or relation.

John