The OWL 2 Full semantics of Disjoint Unions.
c owl:disjointUnionOf SEQ(d_1 ... d_n)
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
- 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.