[ontoiop-forum] DOL finalisation

[John F Sowa]

On 1/2/2018 5:33 PM, Till Mossakowski wrote:
> second-order logic is not outside the scope of DOL. DOL is a
> meta-language that can be used for a variety of logics, provided they
> can be formalised as an institution. Such logics include propositional
> logic, OWL, Common Logic, first-order logic, second-order logic, modal
> logics, hybrid logics, temporal logics, higher-order logics (also
> variants including type constructors, subtypes and/or polymorphism),
> intuitionistic logics, program logics, and many more.

That is very impressive.  Does Hets support all the logics that
DOL can specify?

What kind of performance do you get with some of those logics?

For example, CL allows quantifiers to range over functions and
relations without going beyond first-order proof procedures.
What is the difference in performance of a proof with CL
semantics vs. HOL semantics?

John