[ontoiop-forum] Incompatibilities between DOL and titling in CL

[John F Sowa]

Till, Tara, Terry, et al.,

I had a pressing deadline to meet, which did not allow me to call in.
But this transcript is significant.  I added a cc to the CL list.

> Chat transcript from room: ontoiop_20140924
> ...
> [08:31] TillMossakowski: Tara: it seems that only Common Logic
> without titling and imports would be conformant to DOL. The DOL library
> mechanism needs to be used for titling - otherwise, DOL and CL are just
> incompatible.
>
> [08:35] TerryLongstreth: The foregoing discussion presupposes that
> Common Logic V2 will become the current draft version, and that
> implicitly, that version of CL will be incompatible with the current
> draft of OntoIop
>
> [08:36] TerryLongstreth: So, do we need a harmonization session?
>
> [08:38] TillMossakowski: Tara: it could be useful that libraries
> have a (hierarchical) structure...

I'm revising my previous specification for sorted logics as an annex
to the current draft.  But the mechanism for specifying sorts creates
conflicts with the mechanisms for titling and the import statements that
depend on them.  I won't claim that they're completely inconsistent,
but a mixture of the two would create a huge amount of complexity.

Therefore, I am specifying sort structures (and families of compatible
sort structures) only in terms of the single-universe subset of CL.
I don't use titling, and I assume a simple import statement that is
independent of any nesting.  The same strategy could be adopted for DOL.

A major change in the semantics of the current draft would make it
impossible to meet the deadline of FCD by December.  A simpler
alternative would be a two-part specification in the Section 6:

  1. Split the single universe subset of CL from the mechanism for
     titling and domain restrictions.  Define a very simple import
     statement that does not depend on nesting.  This section would
     be much simpler than the current draft.

  2. In the next section or subsection, specify extensions to the core
     as an option defined on top of the core.  The combination of the
     core plus extensions would be equivalent to the current draft.

  3. The conformance section would allow conformant CL dialects to
     adopt either the core or the extended version.

Implications:

  1. No widely used logics have such a system of titling, importation,
     and domain restrictions.  The core version would be easier to
     implement than the extended version.

  2. Sorted logics, as I'm specifying in the annex or as anyone else
     has specified by other means, are easy to specify on top of the
     core.  But two different mechanisms for restricting domains are
     hard to reconcile.  Therefore, sorted logics would normally be
     defined on top of the core.

  3. DOL would be compatible with logics specified in core CL or with
     sorted logics -- either those specified by the methods in the
     annex or by other methods that do not use the extensions to CL.

  4. Till's point that libraries have a hierarchical structure is
     important.  Instead of using nested importations into CL, a
     simpler approach would be to import a theory in the source
     dialect that has already combined all the desired components.

Method #4 would probably be sufficient for most users.  Applications
that combine theories from multiple dialects could import each one
at the top level, not at nested levels.  In fact, it would be very
risky to mix independently developed modules without a lot of testing.
Anybody who does that testing would map them to the same dialect in
order to do the tests.

John