FullSemanticsDisjointUnions

Goto OWL 2 Full Semantics Page

The OWL 2 Full semantics of Disjoint Unions.

Disjoint Unions

Syntax

 c owl:disjointUnionOf SEQ(d_1 ... d_n)

Semantics

Axiomatic triples:

 owl:disjointUnionOf rdf:type rdf:Property
 owl:disjointUnionOf rdfs:domain owl:Class
 owl:disjointUnionOf rdfs:range rdf:List

Main semantic condition:

 IF
   l is a sequence of d_1,...,d_n over R_I
 THEN
     (c,l) ∈ EXT_I(S_I(owl:disjointUnionOf))
   IF AND ONLY IF
     c ∈ IOC,
     d_1, ..., d_n ∈ IOC,
     CEXT_I(c) = CEXT_I(d_1) ∪ ... ∪ CEXT_I(d_n),
     CEXT_I(d_i) ∩ CEXT_I(d_k) = ∅ for 1 ≤ i < k ≤ n

Considerations

• The semantics are reasonably aligned with the respective semantics of OWL 2 DL.
• Note that in OWL DL, a disjoint union assertion is an axiom, not a class expression (the latter would be nonsensical). But in OWL Full, this distinction is not so clear.
• The style of definition of the main semantic condition matches the repaired style of definition of the OWL 1 Full semantics for owl:unionOf.
• The semantics for owl:disjointUnionOf is straightforward and without alternative once the semantics for 'owl:unionOf' is known.

Goto OWL 2 Full Semantics Page