- From: Peter F. Patel-Schneider <pfps@research.bell-labs.com>
- Date: Tue, 09 Sep 2008 09:29:42 -0400 (EDT)
- To: schneid@fzi.de
- Cc: public-owl-wg@w3.org, team-owl-chairs@w3.org

I noticed that there are some (partial) comprehension principles in Section 4 of the OWL 2 Full Semantics document. I think that the semantics would be cleaner if these were removed, and comprehension-free IFF semantic conditions were provided for all OWL 2 DL axioms. 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))

Received on Tuesday, 9 September 2008 13:34:12 UTC