FullSemanticsNaryAxioms

Goto OWL 2 Full Semantics Page

---

The OWL 2 Full semantics of the n-ary axioms.

The RDF syntax of OWL 1 contains a construct, owl:AllDifferent, which allows to state for a whole set of entities that they are pairwise different. OWL 2 adds additional constructs of this type for other kinds of axioms.

The additional axioms are owl:AllDisjointClasses and owl:AllDisjointProperties.

Note: It is currently unclear whether the remaining n-ary axioms for equivalent classes and properties will receive an RDF syntax. They are listed here, but a warning is added.

The members property

The property 'owl:members' is used by all the "All*" constructs.

Syntax

 x owl:members SEQ(y_1 ... y_n)

Semantics

Axiomatic Triples:

 owl:members rdf:type rdf:Property
 owl:members rdfs:domain rdfs:Resource
 owl:members rdfs:range rdf:List

Note: The domain is rdfs:Resource, since there is currently no common super class for the different "All*" classes.

All Same Individuals

Warning: Currently not part of OWL 2.

Syntax

 x rdf:type owl:AllSameIndividual
 x owl:members SEQ(y_1 ... y_n)

Semantics

Axiomatic triples:

 owl:AllSameIndividual rdf:type rdfs:Class

Main semantic condition:

 IF
   l is a sequence of y_1, ..., y_n over IOT,
   x ∈ CEXT_I(S_I(owl:AllSameIndividual)),
   (x,l) ∈ EXT_I(S_I(owl:members))
 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:AllSameIndividual)),
   (x,l) ∈ EXT_I(S_I(owl:members))

All Different Individuals

This construct already exists in OWL 1. See the corrected OWL 1 Full semantics.

All Equivalent Classes

Warning: Currently not part of OWL 2.

Syntax

 x rdf:type owl:AllEquivalentClasses
 x owl:members SEQ(y_1 ... y_n)

Semantics

Axiomatic triples:

 owl:AllEquivalentClasses rdf:type rdfs:Class

Main semantic condition:

 IF
   l is a sequence of y_1, ..., y_n over IOT,
   x ∈ CEXT_I(S_I(owl:AllEquivalentClasses)),
   (x,l) ∈ EXT_I(S_I(owl:members))
 THEN
   y_1, ..., y_n ∈ IOC,
   CEXT_I(y_i) = CEXT_I(y_k) for 1 ≤ i < k ≤ n 

Comprehension principle:

 IF
   l is a sequence of y_1, ..., y_n over IOC,
   CEXT_I(y_i) = CEXT_I(y_k) for 1 ≤ i < k ≤ n
 THEN ∃ x:
   x ∈ CEXT_I(S_I(owl:AllEquivalentClasses)),
   (x,l) ∈ EXT_I(S_I(owl:members))

All Disjoint Classes

Syntax

 x rdf:type owl:AllDisjointClasses
 x owl:members SEQ(y_1 ... y_n)

Semantics

Axiomatic triples:

 owl:AllDisjointClasses rdf:type rdfs:Class

Main semantic condition:

 IF
   l is a sequence of y_1, ..., y_n over IOT,
   x ∈ CEXT_I(S_I(owl:AllDisjointClasses)),
   (x,l) ∈ EXT_I(S_I(owl:members))
 THEN
   y_1, ..., y_n ∈ IOC,
   CEXT_I(y_i) ∩ CEXT_I(y_k) = ∅ for 1 ≤ i < k ≤ n 

Comprehension principle:

 IF
   l is a sequence of y_1, ..., y_n over IOC,
   CEXT_I(y_i) ∩ CEXT_I(y_k) = ∅ for 1 ≤ i < k ≤ n 
 THEN ∃ x:
   x ∈ CEXT_I(S_I(owl:AllDisjointClasses)),
   (x,l) ∈ EXT_I(S_I(owl:members))

All Equivalent Properties

Warning: Currently not part of OWL 2.

Syntax

 x rdf:type owl:AllEquivalentProperties
 x owl:members SEQ(y_1 ... y_n)

Semantics

Axiomatic triples:

 owl:AllEquivalentProperties rdf:type rdfs:Class

Main semantic condition:

 IF
   l is a sequence of y_1, ..., y_n over IOT,
   x ∈ CEXT_I(S_I(owl:AllEquivalentProperties)),
   (x,l) ∈ EXT_I(S_I(owl:members))
 THEN
   y_1, ..., y_n ∈ IOOP,
   EXT_I(y_i) = EXT_I(y_k) for 1 ≤ i < k ≤ n 

Comprehension principle:

 IF
   l is a sequence of y_1, ..., y_n over IOOP,
   EXT_I(y_i) = EXT_I(y_k) for 1 ≤ i < k ≤ n 
 THEN ∃ x:
   x ∈ CEXT_I(S_I(owl:AllEquivalentProperties)),
   (x,l) ∈ EXT_I(S_I(owl:members))

All Disjoint Properties

Syntax

 x rdf:type owl:AllDisjointProperties
 x owl:members SEQ(y_1 ... y_n)

Semantics

Axiomatic triples:

 owl:AllDisjointProperties rdf:type rdfs:Class

Main semantic condition:

 IF
   l is a sequence of y_1, ..., y_n over IOT,
   x ∈ CEXT_I(S_I(owl:AllDisjointProperties)),
   (x,l) ∈ EXT_I(S_I(owl:members))
 THEN
   y_1, ..., y_n ∈ IOOP,
   EXT_I(y_i) ∩ EXT_I(y_k) = ∅ for 1 ≤ i < k ≤ n 

Comprehension principle:

 IF
   l is a sequence of y_1, ..., y_n over IOOP,
   EXT_I(y_i) ∩ EXT_I(y_k) = ∅ for 1 ≤ i < k ≤ n 
 THEN ∃ x:
   x ∈ CEXT_I(S_I(owl:AllDisjointProperties)),
   (x,l) ∈ EXT_I(S_I(owl:members))

Considerations

• Special case 'owl:AllDifferent'
  • Perhaps there should be aliases to align the names of the URIs:
    • 'owl:AllDifferentIndividuals' as an equivalent class to owl:AllDifferent. In this case it would not be necessary to specify any further semantics for this alias class.
    • 'owl:members' can be made a super property of 'owl:distinctMembers'.
• It is questionable whether there should be special names for the sets which are the class extensions of each "*All" class.
  • OWL 1 Full gives the class extension of owl:AllDifferent the name "IAD".
  • A naming scheme could be (regular expression): "IA?(E|D)(O|C|OP|DP)"
• Perhaps there should be a common class for all "All*" classes:
  • then the axiomatic triples for the classes could be of the form "All* subClassOf CommonClass"
  • then the domain of owl:members would be more specific (currently rdfs:Resource)
  • This would somehow mirror the situation for Restrictions. However, restrictions are distinguished by a property name, while "All*" constructs are distinguished by their class name. So a common class for all "All*" constructs seems less relevant.
• The main semantic conditions are "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 principles provide in each case. Thus "IFF" semantics would be redundant.

---

Goto OWL 2 Full Semantics Page