[ontoiop-forum] DOL finalisation

Wed Dec 27 15:17:30 CET 2017

On 12/21/2017 07:50 PM, Pat Hayes wrote:
> 
> 
>> On Dec 21, 2017, at 9:54 AM, rick <rick at rickmurphy.org> wrote:
>>
>> How about it, Pat?
>>
>> No derivations for "Common Logic"?
>>
>> ISO 24707 actually has no inference rules or proof theory at all,
>> correct? How can they be "out of scope" for a logic?
> 
> Did anyone suggest they are? 

You excluded them in 24707, 1 Scope which reads in part as follows:

"The following are outside the scope of this International Standard:
 * the specification of proof theory or inference rules; "

It's not logic without them.

>> Shouldn't the ISO 24707 authors have released a Common LISP library by
>> now? It's been 10 years.
> 
> The CL effort was done pro bono, and AFAIK none of the authors have funding to work on it further. I certainly have not. Anyone who is interested is welcome to develop CL inference engines or other software, of course. 

Ten years gone and there's no reference implementation, right?

We are told that HETS parses CLIF syntax, but "handles" sequence markers
in second order logic, likely as polymorphic list types.

A consumer of 24707 and standards which depend on it assume significant
risk.

>> Fabian, Annex D is only informative, but the following sentence may be
>> naively interpreted to mean that second order logic is required, or
>> somehow provided.
>>
>> "Note that sequences are essentially a non-first-order feature that
>>
>> can be expressed in second-order logic.”
> 
> Well, that sentence is of course true.

Really? Where would I find sequence markers in the literature on
second-order logic? Reference please.

Assuming a reference, the sentence would be equally true in let's say
the calculus of constructions, right?

Everything that has lists, right?

> The mapping to Lw1w was not noticed until after that was written. We had a strong intuition that second-order was too strong, which is why this says 'can be expressed’ rather than ‘requires’. 

There's no mapping and there's no claim of induction related to sequence
markers in 24707. 24707 has a vague reference to fix points.

And all we've read is a post-hoc claim of an unspecified "induction
principle."

There's no proof, or inference rules, and there's no reference
implementation. Given the related "handle" claim, it sounds like
"requires" rather than "can be expressed" to me.

> If someone reads that sentence in the way you imply, above, then I would suggest they are not competent to read a formal specification. 

That seems pervasive around standards organizations.

>>
>> This is an example of how misinformation is being circulated about
>> "Common Logic." I have discussed this before at OMG.
>>
>> How do you respond to the fact that Java and C# provide parametric
>> polymorphism, but CL and DOL do not?
> 
> With a puzzled frown, not understanding what possible relevance Java or C++ have to anything in this entire discussion (or in ISO 24707)

They have lists similar to those in second order logic which seem to be
required to implement sequence markers in 24707.

Turn that frown upside down.

--
Rick

> Pat
> 
>>
>> Good to see folks promoting Goguen's work though.
>>
>> --
>> Rick
>>
>> On 12/20/2017 07:00 PM, rick wrote:
>>> Maybe Pat can show the derivations to avoid further misunderstanding.
>>>
>>> --
>>> Rick
>>>
>>> On 12/20/2017 05:32 PM, Pat Hayes wrote:
>>>> I hadn’t seen that diagram before. I believe that it is inaccurate to describe CL as having ‘some second-order constructs’. Sequence markers take CL outside FO expressivity, but not to second-order. CL with sequence markers is in fact a subset of the infinitary logic Lw1-w which allows countably infinite conjunctions. This is a long way short of full second-order logic. If one restricts CL (Lw1-w) so that sequence markers (infinite conjunctions) occur only on the LHS of sequents, it is first order. So sequence makers can be used in ontologies (ie as ‘axioms’) without going beyond FO expressivity. 
>>>>
>>>> Pat
>>>>
>>>>> On Dec 20, 2017, at 7:01 AM, John F Sowa <sowa at bestweb.net> wrote:
>>>>>
>>>>> Congratulations to everyone working on the DOL project.
>>>>>
>>>>> From Fabian via ontoiop-forum,
>>>>>> Good news concerning the standardisation of DOL! During the last
>>>>>> OMG Technical Meeting the Architecture Board approved the changes
>>>>>> that we made to DOL during the “Finalisation Phase” (which in our
>>>>>> case lasted 2 years). Hence, we cleared the last major hurdle on
>>>>>> our way to the release of DOL 1.0. I expect that this will happen
>>>>>> in February 2018.
>>>>>
>>>>> And Fabian, I'm sending a copy of this note to Ontolog Forum, and
>>>>> I also attached a copy of an earlier diagram (dol.jpg).
>>>>>
>>>>> Does this diagram reflect the current version?  If so (or not),
>>>>> could you please send the URL of the latest documentation to
>>>>> Ontolog Forum?
>>>>>
>>>>> And is software available for the various mappings in that diagram?
>>>>>
>>>>> John
>>>>> <dol.jpg>
>>>>> _________________________________________________________________
>>>>> 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
>>>>
>>>>
>>>>
>>>> _________________________________________________________________
>>>> 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
>>>>
>>
>>
> 
> 
> 
> 