Re: [SWC] comments/review SWC - part3

Axel Polleres wrote:
> This part 2 of the review from
> http://lists.w3.org/Archives/Public/public-rif-wg/2008Jun/0126.html
> covers Section 4 which wasn't covered in the first review.
> More comments on the RIF-OWL embeddings in the Appendix to follow.
> 
> Axel

Here goes part 3 ... as a continuation of

http://lists.w3.org/Archives/Public/public-rif-wg/2008Jun/0211.html

  still not entirely finished, I still have to check the "Normalized 
Combination Embedding Lemma" proof and onwards... when I got some sleep, 
already too late here for me to think clearly.

Axel


-- 
Dr. Axel Polleres, Digital Enterprise Research Institute (DERI)
email: axel.polleres@deri.org  url: http://www.polleres.net/

Everything is possible:
rdfs:subClassOf rdfs:subPropertyOf rdfs:Resource.
rdfs:subClassOf rdfs:subPropertyOf rdfs:subPropertyOf.
rdf:type rdfs:subPropertyOf rdfs:subClassOf.
rdfs:subClassOf rdf:type owl:SymmetricProperty.

Section 8.2:
========

*) "such as disjunction in negation. "
->
"such as disjunction, negation, and quantification."

(even if you don't want to add quantification, at least change the "in" to an "and")

*) What are "plain literals not in the lexical space of the xs:string datatype"?
Can you give me an example?

Section 8.2.1:
=========

*) "datavaluedPropertyID" -> "dataValuedPropertyID"
"individualvaluedPropertyID" -> "individualValuedPropertyID"

*) the OWL DLP is strictly speaking not DLP but our OWL^-, right? because you allow oneOf on the L-side.
 What is the difference between OWL DLP and OWL-R DL in the OWL2 WG...? Is there a difference except that the grammar is different (didn't check in all detail). I would put this at risk and add a note that we might want to reconcile these fragments in the final version, or at least that the differences (if any) will be clarified, 
I could volunteer to have a look into this.

*) Also, we should consider OWL-R Full, probably. I could volunteer to have a look into this. In general, I think we should find a way to keep a door open for ... even if this is after our own LC, to add some reconciliation with the OWL WGs results, when they are finished... I don't know how and whether the W3C procedures allow this, but it would be odd to have the two specs being developed in practically parallel and then one only referring to the original OWL. (This is more a question to Sandro than to Jos, BTW...)

Section 8.2.2:
=========

*) row 3, and row 4: It would be good to remark that the mappings from b to b' and from c to c' shall be bijections,  because if this step isn't reversible than the whole embedding doesn't make too much me. 
So, instead of 
  "b ... b' ... where b' is a constant symbol, obtained from b that doesn't occur in the original document or the ontologies, and that is not used as a binary predicate symbol in the translation"
I would suggest to write:
  "b ... tr'(b) ... where tr' is an arbitrary bijection that maps constant symbols in the original document or ontologies to "fresh" constant symbols that are not used as constant, function, or predicate  symbols in the original document, ontologies or  elsewhere in the translation. That is, tr' is a function that maps all constant symbols uniquely into new constant not appearing in the  original document or ontologies."

tr' can be used similarly than for the c -> c' mapping, for class names, also, you can reuse tr' and tr'^-1 (since it is a bijection) in the proof of the Lemma later on than, making it cleaner to read.

That is cleaner/clearer. (p.s. I think I had a similar remark in one of my earlier reviews, but no concrete solution, don't remember where at the moment... :-( , shall check).

*) Definition  dl-entails:

 "if for every DL-semantic multi-structure I that is a model of R holds that TValI(φ)=t."
->
 "if for every DL-semantic multi-structure I that is a model of R it holds that TValI(φ)=t."

*) in the lemma, the link to "DL-condition" doesn't work.

*) In the proof of the Lemma, you can use tr' as defined above:
"for every constant symbol c' used as unary or binary predicate symbol in tr(R) or tr(φ) that is obtained from a constant symbol c that occurs in R or φ, I*C( c')=IC(c); I*C(c)=I*C(c) for every other constant symbol c;"
->
"for every constant symbol c' = tr'(c) used as unary or binary predicate symbol in tr(R) or tr(φ), i.e. that is obtained from a constant symbol c that occurs in R or φ, I*C( c')=IC(c); I*C(c)=I*C(c) for every other constant symbol c;"

... or probably you can just even more simple write:

I*_C( c )=I_C( tr^-1(c) )


*) It seems to me that the Def of I* is sometimes not complete in the proof:
E.g. inthe secont bullet:
 "if I_truth(IF(IC(c'))(k))=t, I*frame'(k)((IC(rdf:type), IC(c))=<tt>t</tt>"
->
 "if I_truth(IF(IC(c'))(k))=t, then I*frame'(k)((IC(rdf:type), IC(c))=<tt>t</tt>, and I*frame'(k)((IC(rdf:type), IC(c))=<tt>f</tt> otherwise."

the "and <tt>f</tt> otherwise" is missing also in the thid bullet, it seems, otherwise I* seems
to be incompletely defined, and also the  "only if" direction in  (+) doesn't seem to work.

*) I don't like the notation (+), but have no better idea, so well.

*) There is a typo somewhere here: "derived from constants b≠ tt>rdf:type</tt>"

*) with tr' you could probably drop 
"Let B be the set of constant symbols b' that are derived from constants b≠ rdf:type [...]"
and whenever you talk about b' in B instead talk about "b in the range of tr'()" or simply
say "for every constant symbol b not appaering in the original document or ontologies" 
(because that is where tr' maps to)... I hope it is clear what I mean here.

*) There is a typo where "&phi" should be "&phi;" in the (<=) direction.

Section 8.2.3.1:
==========

*) In the normalization table, row 5, why do you need: "X is a classID or value restriction" ...
What else could X be and where is this else case covered in the translation? Make this clearer, by writing

"If X is a classID or value restriction, otherwise see row 6"

*) similar for row 8 and 13, so here I would rather write:

instead of 
"b is an individualID or dataLiteral"
->
"If b is an individualID or dataLiteral, otherwise see row 7"
(actually, it would make sense to switch rows 8 and 7, because the "otherwise" case is before here, which is odd)

instead of
"X is a description that does not contain intersectionOf"
->
"If X is a description that does not contain intersectionOf, otherwise see row 14"

Section 8.2.3.2:
==========
*) "The embedding extends the embedding function tr: the embeddings of IRIs and literals is as defined in the Section Embedding Symbols."

Why a colon here? Looks odd. "The embedding extends the embedding function tr. The embeddings of IRIs and literals is as defined in the Section Embedding Symbols."

*) I didn't check the translation table in 8.2.3.2 in detail, but I assume it is based on the original table we did in the OWL^- document? If so, I am fine with it, having checked and reviewed several versions of it already.
I again have some troubles understanding whether the third row is conditions or remarks, it seems row 13 should go first, i.e. be row 11, and its condition should say "otherwise see rows 12-18), then row 11 should be 12 (where the condition should say "otherwise see row 13"), etc...

*) Where does this R<sup>OWL-DL</sup> ruleset come from? Which fragment of OWL does it cover? Was that defined anywhere before in some external literature? (just for interest, if so, maybe worthwhile to add an external explanatory pointer, or rationalize the rules somehow)

 ... I will check the proof of the for the "Normalized Combination Embedding Lemma" and onwards hopefully tomorrow.