- From: Michael Schneider <schneid@fzi.de>
- Date: Mon, 15 Sep 2008 15:34:20 +0200
- To: "Peter F. Patel-Schneider" <pfps@research.bell-labs.com>, "Jie Bao" <baojie@cs.rpi.edu>
- Cc: <public-owl-wg@w3.org>
- Message-ID: <0EF30CAA69519C4CB91D01481AEA06A0B98CC1@judith.fzi.de>
Hi Peter and Jie,
finally, here is my answer to your review comments concerning those semantic conditions, which are split into two "IF" conditions, and where the second part has an existential variable.
Jie Bao wrote as a review comment:
"""
I found many conditions in this section are defined
as comprehension rules (usually in the "iff" form).
Will it be better to move all the comprehension ones
into section 6, together with existing comprehension
conditions?
"""
And Peter F. Patel-Schneider wrote per email on September 09, 2008:
>I noticed that there are some (partial) comprehension principles in
>Section 4 of the OWL 2 Full Semantics document.
(The rest of the mail follows below.)
All these are not meant to be comprehension principles, although they look so, because they contain an existentially quantified variable. Sub property chains, the n-ary axioms ("All*"), and the negative property assertions are axioms in OWL 2 DL, and I wanted to define IFF conditions for them in Full just as for every other DL axiom. But these particular axioms have a "root node" in their RDF syntax, which has to be provided somehow. I "create" it by the existential. That's a simple and effective approach, which keeps the treatment local (no need to deal with it in different parts of the document), and which doesn't hurt too much the main structure of the semantic condition.
For the latter claim to see, imagine that the RDF syntax of sub property chains would not contain a root node, as in
q owl:subsumesPropertyChain (p1...pn)
I would define the following IFF semantic condition for this alternative form:
IF l sequence of p1...pn in IR THEN
<q,l> in IEXT(IS(owl:subsumesPropertyChain))
IFF
q, p1, ..., pn in IP,
IEXT(p1) o ... o IEXT(pn) sub IEXT(q)
This can be equivalently split into the following two semantic conditions:
- IF
l sequence of p1...pn in IR,
<q,l> in IEXT(IS(owl:subsumesPropertyChain))
THEN
q, p1, ..., pn in IP,
IEXT(p1) o ... o IEXT(pn) sub IEXT(q)
- IF
l sequence of p1...pn in IP,
q in IP,
IEXT(p1) o ... o IEXT(pn) sub IEXT(q)
THEN
<q,l> in IEXT(IS(owl:subsumesPropertyChain))
Now compare this with the current two semantic conditions for the multi-triple RDF encoding:
- IF
l sequence of p1...pn in IR,
<x,q> in IEXT(IS(rdfs:subPropertyOf)),
<x,l> in IEXT(IS(owl:propertyChain))
THEN
q, p1, ..., pn in IP,
IEXT(p1) o ... o IEXT(pn) sub IEXT(q)
- IF
l sequence of p1...pn in IP,
q in IP,
IEXT(p1) o ... o IEXT(pn) sub IEXT(q)
THEN
EXISTS x in IR,
<x,q> in IEXT(IS(rdfs:subPropertyOf)),
<x,l> in IEXT(IS(owl:propertyChain))
These two IF semantic conditions have almost the same basic form as the split semantic condition for the single-triple variant, except for the additional "EXISTS x in IR" premise. IMHO, that's a pretty small difference, and the "EXISTS x" just does enough to treat the "missing root node" issue. Also, this approach will probably work in the same form for every case where there is a root node for some axiom; at least, it does work this way for all current cases in OWL 2. Btw, I don't see a technical reason for not having two separate "IF" conditions instead of a single "IFF" condition /always/. The reason for the single "IFF" conditions is purely editorial: It takes less space to write them down, and it keeps those things together, which belong to the same language construct.
Compared with this, Peter's proposal below seems more complicated and not less unusual looking to me:
(1) It is a "non-local" treatment which affects three different parts of the document: The main semantic condition for the language feature, the "Classes" and "Properties" tables, and the comprehension principles.
(2) It introduces a sort of IFF condition, which does not occur elsewhere in the Full Semantics: Denotations of triples containing the language feature's vocabulary occur on both sides of the semantic condition, e.g.:
> x in ICEXT(IS(owl:NegativePropertyAssertion))
> <x,u> in IEXT(IS(owl:sourceIndividual))
> <x,p> in IEXT(IS(owl:assertionProperty))
> <x,w> in IEXT(IS(owl:targetIndividual))
> IFF
> <x,u> in IEXT(IS(owl:sourceIndividual))
> <x,p> in IEXT(IS(owl:assertionProperty))
> <x,w> in IEXT(IS(owl:targetIndividual))
> <u,w> not in IEXT(p)
I don't say that this is wrong, because it's technically perfectly allowed. But I followed a design idea to have the semantic conditions look similar to typical interpretations, where you have a syntactic expression on the LHS, and its set-theoretic interpretation on the RHS (as, for example, in the DL semantics). Of course, the Full Semantics works a bit different, since in OWL Full semantic conditions have their consequent /and/ their antecedent in the interpretation space. But I find the above approach at least confusing. Also, having the "triples" on the RHS makes it hard for the right-to-left side to fire. In practice, if the regarded RDF graph does not already contain these triples, the right-to-left side needs the help of a comprehension principle to fire. And if these triples are already in the graph, then the right-to-left side isn't needed anyway. Well, /almost/ not necessary, this brings us to my next point.
(3) The semantic conditions in the "Properties" class are weakened in order to help make the proposed IFF conditions into "real" IFF conditions. In the example cited above, if the domain of owl:sourceIndividual would be ICEXT(IS(owl:NegativePropertyAssertion)), as it is the case at the moment, then the IFF condition would effectively be an ONLY-IF condition, since the right-to-left implication would be trivially true. I don't think that we should change the domain and range of the vocabulary denotations, just to receive "real" iff conditions, but maybe I missed something here?
I would also have some trouble with having the right-to-left sides as comprehension principles, as they differ from the current comprehension principles for lists and class expressions in that their premises are more demanding. But I don't want to extend this mail any more. My claim is that the current approach is more simple and straightforward, although I agree that it is a bit ugly and might even be confusing. To at least address the problem of possible confusion, I have now added some introductory text to the beginning of the "Semantic Conditions" section, which in particular addresses the "existential" semantic conditions. Here is the diff:
<http://www.w3.org/2007/OWL/wiki/index.php?title=RDF-Based_Semantics&diff=12926&oldid=12913>
Please tell me whether this is ok for you or not.
Cheers,
Michael
>This would require the following changes:
>
>1/ Remove all partial comprehension principles from Section 4, i.e.,
> remove the second halves of Table 4.11, 4.13, and 4.17. The
> comprehension principles in Section 6 would have to be augmented to
> make up for these removals.
>
>2/ Change the domain of owl:distinctMembers, owl:assertionProperty,
> owl:sourceIndividual, owl:targetIndividual, and owl:targetValue to
> IR, to allow for comprehension-free IFF semantic conditions for their
> axioms.
>
>3/ Provide comprehension-free IFF conditions for n-ary axioms, somewhat
> similar to the one already existing for disjointUnionOf:
>
> Table 4.13 N-ary Axioms
> if l sequence of u1, ..., un in IR then
> - x in ICEXT(IS(owl:AllDifferent))
> <x,l> in IEXT(IS(owl:members))
> IFF
> <x,l> in IEXT(IS(owl:members))
> u1 /= uk for 1<=i<k<=n
> - same for owl:distinctMembers
> - x in ICEXT(IS(owl:AllDisjointClasses))
> <x,l> in IEXT(IS(owl:members))
> IFF
> <x,l> in IEXT(IS(owl:members))
> ICEXT(ci) ^ ICEXT(ck) = {} for 1<=i<k<=n
> - similarly for AllDisjointProperties
>
>4/ Provide comprehension-free IFF conditions for negative property
> assertions:
>
> Table 4.17: Negative Property Assertions
> - x in ICEXT(IS(owl:NegativePropertyAssertion))
> <x,u> in IEXT(IS(owl:sourceIndividual))
> <x,p> in IEXT(IS(owl:assertionProperty))
> <x,w> in IEXT(IS(owl:targetIndividual))
> IFF
> <x,u> in IEXT(IS(owl:sourceIndividual))
> <x,p> in IEXT(IS(owl:assertionProperty))
> <x,w> in IEXT(IS(owl:targetIndividual))
> <u,w> not in IEXT(p)
> - x in ICEXT(IS(owl:NegativePropertyAssertion))
> <x,u> in IEXT(IS(owl:sourceIndividual))
> <x,p> in IEXT(IS(owl:assertionProperty))
> <x,w> in IEXT(IS(owl:targetValue))
> IFF
> <x,u> in IEXT(IS(owl:sourceIndividual))
> <x,p> in IEXT(IS(owl:assertionProperty))
> <x,w> in IEXT(IS(owl:targetValue))
> p in IDP
> <u,w> not in IEXT(p)
>
>5/ Provide comprehension-free IFF semantic conditions for reifications
> needed for annotations:
>
> Table 4.18: Reification for Annotation
> - x in ICEXT(IS(owl:Axiom))
> <x,u> in IEXT(IS(owl:subject))
> <x,p> in IEXT(IS(owl:predicate))
> <x,w> in IEXT(IS(owl:object))
> iff
> <x,u> in IEXT(IS(owl:subject))
> <x,p> in IEXT(IS(owl:predicate))
> <x,w> in IEXT(IS(owl:object))
> <u,w> in IEXT(p))
> - x in ICEXT(IS(owl:Annotation))
> <x,u> in IEXT(IS(owl:subject))
> <x,p> in IEXT(IS(owl:predicate))
> <x,w> in IEXT(IS(owl:object))
> iff
> <x,u> in IEXT(IS(owl:subject))
> <x,p> in IEXT(IS(owl:predicate))
> <x,w> in IEXT(IS(owl:object))
> p in IAP
> <u,w> in IEXT(p))
--
Dipl.-Inform. Michael Schneider
FZI Forschungszentrum Informatik Karlsruhe
Abtl. Information Process Engineering (IPE)
Tel : +49-721-9654-726
Fax : +49-721-9654-727
Email: Michael.Schneider@fzi.de
Web : http://www.fzi.de/ipe/eng/mitarbeiter.php?id=555
FZI Forschungszentrum Informatik an der Universität Karlsruhe
Haid-und-Neu-Str. 10-14, D-76131 Karlsruhe
Tel.: +49-721-9654-0, Fax: +49-721-9654-959
Stiftung des bürgerlichen Rechts
Az: 14-0563.1 Regierungspräsidium Karlsruhe
Vorstand: Rüdiger Dillmann, Michael Flor, Jivka Ovtcharova, Rudi Studer
Vorsitzender des Kuratoriums: Ministerialdirigent Günther Leßnerkraus
Received on Monday, 15 September 2008 13:35:02 UTC