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.

Replace
>..., subset of RI.
by 
>..., and is a subset of RI.

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].
"

Replace 
>... that are correspond to constructors ...
by
"... that correspond to constructors ..."

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 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.

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.)

It seems that the last line of the first table, on "l"^^d
can be left out, since it is implied by the RDF Semantics.
Or, leave it in and change the note to
"This condition is also in the RDF model theory", as you do
in the next table also.
By the way, I like the notes that you added to the tables.
These notes, in combination with the new headers of the tables,
improve the readability of this section.

In the first two lines of the same first table, CEXTI(SI(rdfs:Class))
should be replaced by CI, as this is equal and as it is
the more fundamental entity in the RDF Semantics, and as
it simplifies this table.

In the third part of the table
"Characteristics of OWL classes, datatypes, and properties",
"If E is ... then if e is in CEXTI(SI(E)) then"
e should be replaced by c in this header.

In the table "Further conditions on owl:oneOf"
the last conclusions "and CEXTI(x)={y1,...,yn}"
can (and in my view should) be omitted, as they
are already stated in the table before.

The last remark on this section returns to a point we discussed
earlier.  In the semantics of the cardinality restrictions,
v should be taken from IOT union LV (three times).
As mentioned before, there is an immediate proof
that the entity {v in IOT union LV: <u,v> in EXTI(p)}
is a set, which is required since its cardinality is taken.
Also, it is done in exactly the same way in the direct semantics.


Section 5.3

In the table defining OWL Full interpretations, CEXTI(SI(rdfs:Class))
should be replaced by CI and CEXTI(SI(rdfs:Property)) should be 
replaced by PI, as these entities are equal and are more fundamental
in the RDF Semantics, and since these substitutions simplify
the definition.

Question: why is the definition of 'imports closed' given in this
section?  It is not used in this section.

Delete bracket ) following "OWL vocabulary".


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).

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



Herman

Received on Wednesday, 26 March 2003 09:11:40 UTC