[ontoiop-forum] DOL finalisation

[John F Sowa]

Till,

Thanks for the answers to my questions and Pat's questions.
Those answers and the diagram on the Hets web site clarify
many of the issues:  http://hets.eu/

As the diagram shows, Hets can support a large family of theorem
provers for various logics.  But can it support two or more
theorem provers for different aspects of the same proof?

For example, the method of using hybrid theorem provers began
in the 1980s with a combination of a description logic for the
T-Box and FOL for the A-Box.  Does Hets support such combinations?

Sorted logics can be considered hybrids, since they combine
a DL method and an FOL method of theorem proving.  Could Hets
be used to create a sorted theorem prover by combining two
such theorem provers?  If not directly, could it combine them
after suitable modifications to each?

> By contrast, most HOL logics include lambda abstraction, which
> makes unification and thus resolution much harder. So the crucial
> feature making HOL much harder is lambda abstraction, which
> is not (and cannot be) present in CL.

That's an important point.  But some languages use the keyword 'lambda'
as a purely syntactic marker for defining functions.  For example:

    (= f (lambda (x y) ("some expression that uses x and y")))

This is a convenient notation in LISP and other languages,
but they don't use any of the mechanisms of lambda calculus.
Is it true that this syntax could be used in CL without going
beyond a first-order style of theorem proving?

John