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
x rdf:type owl:AllDifferent x owl:distinctMembers SEQ(y_1 ... y_n)
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
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))
- 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"