Comment on OWL 2 Full Semantics

• 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
• Message-Id: <20080909.092942.24187936.pfps@research.bell-labs.com>

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