FullSemanticsAllDifferent

Goto OWL 2 Full Semantics Page

The corrected OWL 1 Full semantics of owl:AllDifferent.

Note: The semantics for this language construct is broken in OWL 1 Full, since the main semantic condition misses. This error will be fixed on this page.

All Different Individuals

Syntax

 x rdf:type owl:AllDifferent
 x owl:distinctMembers SEQ(y_1 ... y_n)

Semantics

Axiomatic triples (already in OWL 1 Full):

 owl:AllDifferent rdf:type rdfs:Class

Axiomatic triples (missing in OWL 1 Full):

 owl:distinctMembers rdf:type rdf:Property
 owl:distinctMembers rdfs:domain owl:AllDifferent
 owl:distinctMembers rdfs:range rdf:List

Main semantic condition (missing in OWL 1 Full):

 IF
   l is a sequence of y_1, ..., y_n over R_I,
   x ∈ CEXT_I(S_I(owl:AllDifferent)),
   (x,l) ∈ EXT_I(S_I(owl:distinctMembers))
 THEN
   y_i ≠ y_k for 1 ≤ i < k ≤ n 

Comprehension principle:

 IF
   l is a sequence of y_1, ..., y_n over IOT,
   y_i ≠ y_k for 1 ≤ i < k ≤ n
 THEN ∃ x:
   x ∈ CEXT_I(S_I(owl:AllDifferent)),
   (x,l) ∈ EXT_I(S_I(owl:distinctMembers))

Considerations

• The main semantic condition doesn't exist in OWL 1 Full. Its specification has probably simply been forgotten.
• Axiomatic triples have been added for owl:distinctMembers. They miss in OWL 1 Full.
• The main semantic condition is "IF-only" semantics, not "IFF" semantics. The reason is that symmetric IFF semantics would not really be possible, because the back direction would need to introduce an existential variable x. But this is exactly the semantics which the comprehension principle provides. Thus "IFF" semantics would be redundant.
• The axiomatic typing triple for 'owl:distinctMembers' could alternatively be "owl:distinctMembers rdfs:subPropertyOf owl11:members"

Goto OWL 2 Full Semantics Page