[ontoiop-forum] DOL finalisation

[Till Mossakowski]

Am 02.01.2018 um 23:52 schrieb 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?
>
no, of course not. The theoretical framework of institutions has
infinitely many examples.
Here is the list of Hets-supported logics, copied (and slightly edited,
will change that...) from http://hets.eu/
    general-purpose logics: Propositional, QBF, TPTP (FOL), THF (HOL),
CASL (FOL), HasCASL (HOL), Isabelle/HOL
    logical frameworks: Isabelle, LF, DFOL
    modeling languages: Meta-Object Facility (MOF),
Query/View/Transformation (QVT), UML class diagrams, state machines,
sequence diagrams
    ontologies and constraint languages: OWL, CommonLogic, RelScheme,
ConstraintCASL
    reactive systems: CspCASL, CoCASL, ModalCASL, ExtModal (modal,
hybrid and temporal logic), Maude
    programming languages: Haskell, VSE (dynamic logic)
    logics of specific tools: Reduce, DMU (CATIA)

> What kind of performance do you get with some of those logics?
Hets' parsing and analysis generally is fast. Theorem proving and such
greatly depends on the theorem provers that you use. Here is a list of
provers that Hets can speak to, again taken from http://hets.eu/

    minisat and zChaff, which are SAT solvers,
    SPASS, Vampire, Darwin, Hyper and MathServe, which are automatic
first-order theorem provers,
    Pellet and Fact++, description logic tableau provers,
    Leo-II and Satallax, automated higher-order provers,
    Isabelle, an interactive higher-order theorem prover,
    CSPCASL-prover, an Isabelle-based prover for CspCASL,
    VSE, an interactive prover for dynamic logic.

>
> 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?
>
I have not checked, but I would guess that proofs for CL are generally
faster than for HOL, because you can use a first-order resolution
prover, or an induction prover if you use sequence markers in a
non-eliminable way. By constrast, 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.

Best, Till
> John
>
> _________________________________________________________________
> To Post: mailto:ontoiop-forum at ovgu.de
> Message Archives: https://listserv.ovgu.de//pipermail/ontoiop-forum
> Config/Unsubscribe:
> https://listserv.ovgu.de/mailman/listinfo/ontoiop-forum
> Community Files (open): http://interop.cim3.net/file/pub/OntoIOp/
> Community Wiki: http://ontoiop.org