FullSemanticsNegativePropertyAssertions

Goto OWL 2 Full Semantics Page

The OWL 2 Full semantics of Negative Property Assertions.

The Domain and Range of a negative property assertion

I suggest that the following entailment does not hold:

 IF 'p' is a data property
 AND 's p t' is NOT true
 THEN t is a data value.

The problem is that it should be allowed to express that a triple 's p t' is not true, if t is known to be not a data value. The above entailment would be a semantic side effect of a negative property assertion, which might lead to heavy problems in certain occations.

More generally, nothing should be learnt about the origin of the LHS and the RHS of a negative property assertion, which isn't already known without.

Common Semantics

Axiomatic triples:

 owl:NegativePropertyAssertion rdf:type rdfs:Class

 owl:sourceIndividual rdf:type rdf:Property
 owl:sourceIndividual rdfs:domain owl:NegativePropertyAssertion
 owl:sourceIndividual rdfs:range rdfs:Resource

 owl:assertionProperty rdf:type rdf:Property
 owl:assertionProperty rdfs:domain owl:NegativePropertyAssertion
 owl:assertionProperty rdfs:range owl:ObjectProperty

 owl:targetIndividual rdf:type rdf:Property
 owl:targetIndividual rdfs:domain owl:NegativePropertyAssertion
 owl:targetIndividual rdfs:range rdfs:Resource   

 owl:targetValue rdf:type rdf:Property
 owl:targetValue rdfs:domain owl:NegativePropertyAssertion
 owl:targetValue rdfs:range rdfs:Resource

Note: The domain and range of 'owl:sourceIndividual' and 'owl:target*' have been deliberately chosen to be rdfs:Resource for the reason given in #The Domain and Range of a negative property assertion.

Negative Object Property Assertions

Syntax

 x rdf:type owl:NegativePropertyAssertion
 x owl:sourceIndividual s
 x owl:assertionProperty p
 x owl:targetIndividual t

Semantics

Main semantic condition:

 IF
   (x,s) ∈ EXT_I(S_I(owl:sourceIndividual)),
   (x,p) ∈ EXT_I(S_I(owl:assertionProperty)),
   (x,t) ∈ EXT_I(S_I(owl:targetIndividual))
 THEN
   x ∈ CEXT_I(S_I(owl:NegativePropertyAssertion)),
   p ∈ IOOP,
   (s,t) ∉ EXT_I(p)

Comprehension Principle: [FIXME: necessary?]

 IF
   s, t ∈ IOT,
   p ∈ IOOP,
   (s,t) ∉ EXT_I(p)
 THEN ∃ x:
   (x,s) ∈ EXT_I(S_I(owl:sourceIndividual)),
   (x,p) ∈ EXT_I(S_I(owl:assertionProperty)),
   (x,t) ∈ EXT_I(S_I(owl:targetIndividual))

Negative Data Property Assertions

Syntax

 x rdf:type owl:NegativePropertyAssertion
 x owl:sourceIndividual s
 x owl:assertionProperty p
 x owl:targetValue t

Semantics

Main semantic condition:

 IF
   (x,s) ∈ EXT_I(S_I(owl:sourceIndividual)),
   (x,p) ∈ EXT_I(S_I(owl:assertionProperty)),
   (x,t) ∈ EXT_I(S_I(owl:targetValue))
 THEN
   x ∈ CEXT_I(S_I(owl:NegativePropertyAssertion)),
   p ∈ IODP,
   (s,t) ∉ EXT_I(p)

Comprehension Principle: [FIXME: necessary?]

 IF
   s ∈ IOT,
   t ∈ LV_I,
   p ∈ IODP,
   (s,t) ∉ EXT_I(p)
 THEN ∃ x:
   (x,s) ∈ EXT_I(S_I(owl:sourceIndividual)),
   (x,p) ∈ EXT_I(S_I(owl:assertionProperty)),
   (x,t) ∈ EXT_I(S_I(owl:targetValue))

Considerations

• The semantics presented here basically conform2 to the respective semantics in OWL 2 DL.
• I think that the typing statement x in owl:NegPropAssertion is better placed in the "THEN" branch, and not in the "IF" branch.
  • This seems to be the typical approach in OWL 1 Full.
  • It has the advantage that the types of the regarded entities do not need to be known, but instead this typing information can be inferred.
• The main semantic conditions should be ONLY-IF conditions. With IFF conditions, there would be an axiom around, together with the existence of a "proxy" individual, for every assertion which is /not/ true.
• Data CP: The premise has to demand that "t in LV_I".
  • Reason: Otherwise, t would be coerced into a data value by the triple "x targetValue t"
  • Discussion: No problem for correspondence theorem, since DL semantics also require t to be a data value

Goto OWL 2 Full Semantics Page