AS & S review: RDFS-compatible OWL semantics

Here is the next part of my review comments on the Semantics 
document:
Section 5 RDFS-Compatible Model-Theoretic Semantics
Version of 16 January

This part of the document is crucial for the semantic
layering of OWL on RDF.  It is perhaps surprising that
after all the work and discussion on this topic, more needs
to be said about several formal aspects to ensure that the 
text becomes completely suitable.

The first point that I want to raise is that many 
small, additional assumptions need to be made on an 
OWL interpretation in order to assure that each use that
is made of the functions EXTI and CEXTI can really be made.
In order to explain this, note that the current text does not 
start from a suitable summary of the RDF Semantics. 
In the second and third paragraph of Section 5.2,
an RDFS interpretation is first described as a three-tuple,
and then, in a "datatyped" version, as a four-tuple.
However, an RDFS interpretation, datatyped or not, is currently
described as a five-tuple, including a set of properties PI as
part of the basic definition.  The domain of the function EXTI
is not all of RI, but only the set PI.  This change was made in 
November (when the RDF Model Theory was renamed to RDF Semantics;
the OWL AS & S document still speaks of RDF MT).
A related point is that the domain of the function CEXTI consists
only of the set of classes CI, which may also not be all of RI 
(this was already the case with the RDF MT version of April).

In view of this, the given summary of RDF semantics should be 
replaced by an up to date and somewhat more extensive summary.
Let me briefly summarize the basic definition of the RDF semantics,
in order to be able to describe the additional assumptions that
need to be made in the OWL semantics, and in order to facilitate 
the replacement of the given summary of the RDF semantics. 
I use the slight adaptation made by Peter of the original notation 
of Pat, however without making many final I's a subscript, of 
course.
An RDFS interpretation of a vocabulary V is a five-tuple consisting 
of:
- a set RI (the universe)
- a set PI subsetOf RI
- a function EXTI : PI -> P(RI x RI) 
- a function SI : V -> RI
- a function LI : {typed literals} -> RI
satisfying many special conditions specified in the RDF Semantics.
(By the way, referring to an earlier part of this review,
note that the P(X) notation for power set is very convenient here.)

Given such an RDFS interpretation, the set of classes is defined
to be
CI := {x in RI: <x,SI(rdfs:Class)> in EXTI(SI(rdf:type))}.
This set is defined to be the domain of the function
CEXTI : CI -> P(RI) 
CEXTI(c) := {x in RI : <x,c> in EXTI(SI(rdf:type))} (c in CI)
These are all the definitions that need to be summarized.
It follows from the complete definition of RDFS interpretation
(actually, it follows already from the definition of RDF 
interpretation) that
(*) CI = CEXTI(SI(rdfs:Class))  and  PI = CEXTI(SI(rdf:Property)).
(The range that I give above to the function CEXTI does not
appear explicitly in the RDF Semantics document, but follows
clearly from what is said there.)

So each table in Section 5.2 needs to be expanded with an 
assumption
SI(E) in CI (in case CEXTI(SI(E)) is used) or 
SI(E) in PI (in case EXTI(SI(E)) is used).

In the second table of Section 5.2 this is easy: each of 
the empty cells in the second column can just be assigned 
the content CI.

In the later tables it is also possible to incorporate the 
required additional assumptions, in the bold header texts.

A simpler and more elegant way to incorporate these additional 
assumptions could be as follows.
The OWL vocabulary at the beginning of Section 5.1.1 
(where it now "appears" with an ellipsis) could be expanded
explicitly, using two disjoint subsets VOWLC and VOWLP (it is 
clear which vocabulary members should go where).  Then the 
required additional assumptions on an OWL interpretation
can be made in one stroke with 
SI(VOWLC) subsetOf CI   and SI(VOWLP) subsetOf PI.


The equations (*) above can be used to simplify many entries
in the tables in Section 5.2, by taking CI or PI instead of 
the expansions in the right-hand sides of these equations.
It should be noted that CI and PI are more fundamental in the
RDF Semantics then these expansions.
Also, the conditions for an OWL interpretation to be OWL Full
become simply IOT = RI, IOC = CI, IOP = PI.


There is a problem with the definition of 
"sequence of y1,...,yn over C".  I can prove that this
definition cannot be suitable.  Namely, in the first application
of this definition, C becomes IOC.  The definition uses
CEXTI(C), so assumes IOC in CI.  In OWL Full, IOC = CI,
so we get CI in CI.  This contradicts the axiom of foundation.
The definition can be repaired by letting yi in C instead
of yi in CEXTI(C).  This seems to be suitable for each use of 
the definition, except perhaps the use in connection with 
distinctMembers: shouldn't it be IOT instead of IOC there?


In my view, the formal definition of an OWL interpretation should
include, in addition to an RDFS interpretation <RI,PI,EXTI,SI,LI>,
the distinguished subsets IOC, IOP, IOT, IOR, IOOP, IODP, IDC,
IAD, and IL of RI.  Otherwise, these sets "fall out of the air".
Each of these 9 subset relationships is implied by the second
table of Section 5.2, except for IAD subsetOf RI, which should
be added to this table.

The second table does not include the inclusion LV subsetOf RI,
which can be assumed by the RDF Semantics, and which would
be appropriate to recall in the table.


The first table in Section 5.2 uses sets IOP, IOC etc. whose 
meaning is not yet clear.  Therefore I propose to move this table
to the third position.  Then, moreover, we get three more coherent 
"groups of tables" in a row:
1. universe/syntactic categories; classes/datatypes/properties
2. the "iff tables": domains/ranges; equivalence
3. the "DL tables": Boolean combinations; restrictions; 
   comprehension principles
I feel that Section 5.2 could use more text to motivate these
different kinds of tables.  For example, can it be 'explained' 
why is there an iff for owl:sameClassAs and owl:disjointWith
but not for owl:complementOf?

In my view, the first condition on oneOf is an unsuitable integration
of dissimilar conditions.  In fact, the next table, which is
completely devoted to oneOf, could be omitted by slightly 
extending the condition in the previous table, as follows:
  ( x in IOC and l is a sequence of y1,...,yn over IOT
  or x in CI and l is a sequence of y1,...,yn over LV )
  and CEXTI(X) = {y1,...,yn}
The first table where oneOf currently appears has two header
lines with bold text.  The first of these lines should be
omitted.


Section 5.1 starts with the following sentence:
"All of the OWL vocabulary is defined on the 'OWL universe', 
which is a collection of RDFS classes that are intended to 
circumscribe the domain of application of the OWL vocabulary: 
owl:Thing, owl:Class and owl:Property."
I read here that 
OWL universe = {owl:Thing, owl:Class and owl:Property}.
However, with the RDF semantics it is inherited that
the set RI is called the universe of the interpretation,
as is also mentioned in the beginning of Section 5.2.
As the word universe is used here in two different ways,
I feel that the wording of the cited sentence should be
adapted to incorporate the connection with RDF semantics.


The table on the semantics of the cardinality restrictions 
does not yet include the corrections which I believe you 
confirmed earlier.
It should be, three times:
   card{v in IOT union LV : <u,v> in EXTI(p)}
(In our earlier discussion I missed the LV part.
In this way, both object properties and datatype properties
are covered, in the correct, intended way.)
Without this addition, formally, there is no set, so
no cardinality can be taken.  Instead, formally, there is 
only a class, not in the sense of OO or RDF or OWL, but 
in the sense of Zermelo-Fraenkel set theory.

I find it confusing, in the definition of separated OWL
vocabulary in Section 5.3.2, to identify a vocabulary
with a partition of it.  I am in favor of omitting the 
= sign, and of speaking of a vocabulary V' with partition
<...>.  This would also affect (improve) the next paragraphs, 
including the statement of Theorem 1.

As to the next definition, of OWL abstract ontology with
separated names, it is not consistent with the first sentence
of Section 2.1, to speak of a set of axioms and facts
in the abstract syntax: it should become a sequence.

In Sections 5.3.1/2, three RDF Graphs should become RDF graphs.

In the definition of OWL DL interpretation, it is awkward to
use the letter n for a vocabulary element, in the third line 
of the table (since n suggests integers).

As to notation, I prefer the standard notation for empty set
instead of {} (this also appeared in earlier sections).