[ontoiop-forum] DOL finalisation

[Till Mossakowski]

John,

Am 03.01.2018 um 17:17 schrieb 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?
>
With Hets, you can only use one theorem prover at a time. Of course, you
can use multiple provers in parallel to attack one goal, but without any
prover cooperation. A certain step towards prover cooperation is to
speculate lemmas and then use a different theorem provers for the lemmas
and the main theorem.
>> 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?
>
If you restrict this to first-order definitions, then it seems harmless
to me (though I cannot see what is gained by this notation).
However, higher-order definitions won't work:
(= russell (lambda (p) (lambda (x) (not (p x)))))
produces an inconsistency.

Best, Till