# 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