Warning:
This wiki has been archived and is now read-only.
FullSemanticsNegativePropertyAssertions
Goto OWL 2 Full Semantics Page
The OWL 2 Full semantics of Negative Property Assertions.
Contents
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