Re: S&AS review: Section 5

>> OWL - Semantics and Abstract Syntax
>> Version of 20 March 2003
>> 
>> As in the other message, I go sequentially through the text.
>> 
>> 
>> Section 5.2
>> 
>> In the introductory sentences and also in the first definition, D
>> is called datatype theory.  This is not consistent with
>> the RDF Semantics document and also not with your own
>> text in Section 3.1: there, a datatype theory is a tuple
>> including D.
>> Therefore, D should be described as being a set of datatypes,
>> in these two places, and also in the beginning of Appendix A.1.
>
>I've changed from D to T.  I can't change to be like the RDF Semantics
>until the RDF datatypes are fixed.
>
>I've added
>
>       (The specifics of datatype theories used here differ from those in
>       the RDF semantics because there are continuing problems with RDF
>       datatyping.  It is hoped that these problems will be resolved
>       during last call, at which time this document will be revised to
>       correspond directly to RDF datatyping.)
>

I agree with these changes concerning datatypes, and with the 
further change by Jim.

>
>> Replace
>> >..., subset of RI.
>> by 
>> >..., and is a subset of RI.
>
>I don't see a place where this is appropriate.

The review version (20 march) had it, and it is no longer there.
This is no problem as this condition is also in a table.

>
>> The current version of the RDF Semantics document
>> clearly defines the domain of ICEXT to be the set IC. 
>> This should be incorporated in the document. 
>> For your convenience, I completely describe the 
>> required changes, also in connection with the appendix.
>
>> Replace the sentence
>> >CEXTI is then defined as CEXTI(c) = ...
>> by the following two sentences:
>> "CI, the set of classes, is defined by
>> CI = {x in RI | <x,SI(rdfs:Class)> is in EXTI(SI(rdf:type)>}.
>> CEXTI is a mapping from CI to P(RI), defined for each
>> c in CI by CEXTI(c) = [exactly what is already in the text].
>> "
>
>I disagree with this characterisation of ICEXT, and will not make these
>changes.
>
Here is the current version of the normative definition,
which clearly states that the domain of ICEXT is IC,
and in which the definition of IC and ICEXT is clearly 
equivalent to what I wrote above:

RDFSemantics>An rdfs-interpretation of V is an rdf-interpretation 
>I of (V union rdfV union rdfsV) with a distinguished subset IC 
>of the universe and a mapping ICEXT from IC to the set of 
>subsets of IR, which satisfies the following semantic 
>conditions and all the triples in the subsequent table, 
>called the RDFS axiomatic triples. 
>[... I list only the first two conditions in the table:]
>x is in ICEXT(y) iff <x,y> is in IEXT(I(rdf:type))
>IC = ICEXT(I(rdfs:Class))

What the current version of S&AS does not yet incorporate
is the domain requirement on ICEXT.
There is no reason not to incorporate now in S&AS the correct 
up-to-date definition of ICEXT.
Your following two 'I disagree's apparently also derive 
from this.


[...]

>
>> The first table, "Conditions concerning the parts of the OWL
>> universe and syntactic categories" needs to be completed
>> in connection with CI:  Each of the 11 empty cells in the
>> first column (SI(E) is in ...) needs to be filled with the
>> set CI.  Otherwise, as discussed before, many invocations
>> of CEXTI that occur later are are not clearly legal.
>
>I disagree.
>
>> I believe that five more lines need to be added to this table,
>> for the following vocabulary elements
>> (the reason is, as before, that otherwise it is not clear
>> that various function invocations occurring later are legal):
>> 
>> If  E is                      .SI(E). .CEXTI(SI(E)).    and
>>   owl:Datarange                 CI       ?      ? subsetof CI
>>   owl:SymmetricProperty         CI       ?      ? subsetof IOP
>>   owl:FunctionalProperty        CI       ?      ? subsetof IOP
>>   owl:InverseFunctionalProperty CI       ?      ? subsetof IOP
>>   owl:TransitiveProperty        CI       ?      ? subsetof IOP
>> Where I put a question mark I leave it open whether you
>> want to define specific sets for these; this would seem 
>> most natural to me.
>
>I disagree.
>
>> There are only two further additions to be made:
>> the entities SI(owl:DeprecatedClass) and SI(owl:DeprecatedClass)
>> need to be put in CI as well.
>> (This is used in the proofs in Appendix A.1.)
>
>Done.

Please point out where you have done this - I cannot find it.

[...]

>
>> Question: why is the definition of 'imports closed' given in this
>> section?  It is not used in this section.
>
>It has to be somewhere, as it is referred to from Test.  It is not used
>elsewhere in the document, so I'm not sure where it should go if it is 
not
>here.

Since this definition seems to interrupt anywhere in Sections 5.1 to 5.4,
it could perhaps best be put in the introduction of Section 5,
just before Section 5.1, with an 'explanation' that there seems to be
no better place, or something like that.

[...]

>> Appendix A.1
>> 
>> This is not a complete review of this appendix.
>> However, in connection with what is discussed above about
>> CI/CEXTI, I looked far enough to ensure that the appendix
>> becomes completely consistent: each invocation of CEXTI
>> done there is legal when the above changes are made.
>> 
>> I noted also that in the proof of Lemma 4, starting with the
>> 6th bullet, very many invocations of the function SI need
>> to be added, in expressions such as CEXTI(rdf:type).
>
>Yuck.  I think that I've fixed them all.  Also for EXTI(rdf:type).
>
>> In the same, long, bulleted list, note that many invocations
>> of CEXTI need to be replaced by EXTI and vice versa.
>> I could list these for you, but I assumed that you can find
>> them quicker yourself, by just using the following rules:
>> - owl/rdf vocabulary element starts with lower case: use EXTI
>> - owl/rdf vocabulary element starts with capital: use CEXTI
>
>No.  This is not correct.  OWL/RDF vocabulary elements that start with
>lower case need a CEXTI to complete the definition of EXTI(SI(rdf:type).
>OWL/RDF vocabulary elements that start with a capital need an EXTI, 
because
>I've defined PI rather expansively to include the denotation of all the
>built-in vocabulary.

OK - I was too quick here.  As I noted, this is not a complete
review of the appendix.  When I come to that, I will look into 
it further.

>
>> Herman
>
>Today's version of the document has been updated to include all these
>changes.
>
>peter
>

Herman

Received on Thursday, 27 March 2003 09:13:14 UTC