Copyright © 2003 W3C^{®} (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark, document use and software licensing rules apply.
This model-theoretic semantics for OWL is an extension of the semantics defined in the RDF semantics [RDF MT], and defines the OWL semantic extension of RDF.
NOTE: The details of this semantics depends on several post-last-call fixes and other changes to the RDF model theory. Most of these changes are not noticable, but several, including the removal of language tags from typed literals and the changes to datatypes, result in noticable changes.
All of the OWL vocabulary is defined on the 'OWL universe', which is a division of part of the RDF universe into three parts, namely OWL individuals, classes, and properties. The class extension of owl:Thing comprises the individuals of the OWL universe. The class extension of owl:Class comprises the classes of the OWL universe. The union of the class extensions of owl:ObjectProperty, owl:DatatypeProperty, owl:AnnotationProperty, and owl:OntologyProperty comprises the properties of the OWL universe.
There are two different styles of using OWL. In the more free-wheeling style, called OWL Full, the three parts of the OWL universe are identified with their RDF counterparts, namely the class extensions of rdfs:Resource, rdfs:Class, and rdf:Property. In OWL Full, as in RDF, elements of the OWL universe can be both an individual and a class, or, in fact, even an individual, a class, and a property. In the more restrictive style, called OWL DL here, the three parts are different from their RDF counterparts and, moreover, pairwise disjoint. The more-restrictive OWL DL style gives up some expressive power in return for decidability of entailment. Both styles of OWL provide entailments that are missing in a naive translation of the DAML+OIL model-theoretic semantics into the RDF semantics.
A major difference in practice between the two styles lies in the care that is required to ensure that URI references are actually in the appropriate part of the OWL universe. In OWL Full, no care is needed. In OWL DL, localizing information must be provided for many of the URI references used. These localizing assumptions are all trivially true in OWL Full, and can also be ignored when one uses the OWL abstract syntax, which corresponds closely to OWL DL. But when writing OWL DL in triples, however, close attention must be paid to which elements of the vocabulary belong to which part of the OWL universe.
Throughout this section the OWL vocabulary will be the disallowed vocabulary from OWL plus the built-in classes, the built-in annotation properties, and the built-in ontology properties.
The semantics of OWL DL and OWL Full are very similar. The common portion of their semantics is thus given first, and the differences left until later.
From the RDF semantics [RDF MT], for V a set of URI references containing the RDF and RDFS vocabulary and T a datatype theory, a T-interpretation of V is a tuple I = < R_{I}, P_{I}, EXT_{I}, S_{I}, L_{I}, LV_{I} >. R_{I} is the domain of discourse or universe, i.e., a set that contains the denotations of URI references. (The specifics of datatype theories used here differ slightly from those in the RDF semantics currently under review. It is expected that these discrepancies will be resolved during last call, following which this document will be revised to correspond directly to RDF datatyping.) P_{I} is a subset of R_{I}, the properties of I. EXT_{I} is used to give meaning to properties, and is a mapping from P_{I} to P(R_{I} × R_{I}). S_{I} is a mapping from V to R_{I} that takes a URI reference to its denotation. L_{I} is a mapping from typed literals to LV_{I}. LV_{I} contains at least all the values for plain literals. CEXT_{I} is then defined as CEXT_{I}(c) = { x∈R_{I} | <x,c>∈EXT_{I}(S_{I}(rdf:type)) }. As well C_{I} is defined as C_{I} = CEXT_{I}(S_{I}(rdfs:Class)). T-interpretations must meet several other conditions, as detailed in the RDF semantics. For example, EXT(S_{I}(rdfs:subClassOf)) must be a transitive relation and the class extension of all datatypes must be subsets of LV_{I}.
Definition: Let T be a datatype theory that includes datatypes for xsd:integer and xsd:string. An OWL interpretation, I = < R_{I}, P_{I}, EXT_{I}, S_{I}, L_{I} >, of a vocabulary V, where V includes the RDF and RDFS vocabularies and the OWL vocabulary, is a T-interpretation of V that satisfies all the constraints in this section.
Note: Elements of the OWL vocabulary that construct descriptions in the abstract syntax are given a different treatment from elements of the OWL vocabulary that correspond to (other) semantic relationships. The former have only-if semantic conditions and comprehension principles; the latter have if-and-only-if semantic conditions. The only-if semantic conditions for the former are needed to prevent semantic paradoxes and other problems with the semantics. The comprehension principles for the former and the if-and-only-if semantic conditions for the latter are needed so that useful entailments are valid.
Conditions concerning the parts of the OWL universe and syntactic categories
If E is | then | Note | ||
---|---|---|---|---|
S_{I}(E)∈ | CEXT_{I}(S_{I}(E))= | and | ||
owl:Class | C_{I} | IOC | IOC⊆C_{I} | This defines IOC as the set of OWL classes. |
rdfs:Datatype | IDC | IDC⊆C_{I} | This defines IDC as the set of OWL datatypes. | |
owl:Restriction | C_{I} | IOR | IOR⊆IOC | This defines IOR as the set of OWL restrictions. |
owl:Thing | IOC | IOT | IOT⊆R_{I} | This defines IOT as the set of OWL individuals. |
owl:Nothing | IOC | {} | ||
rdfs:Literal | IDC | LV_{I} | LV_{I}⊆R_{I} | |
owl:ObjectProperty | C_{I} | IOOP | IOOP⊆P_{I} | This defines IOOP as the set of OWL individual-valued properties. |
owl:DatatypeProperty | C_{I} | IODP | IODP⊆P_{I} | This defines IODP as the set of OWL datatype properties. |
owl:AnnotationProperty | C_{I} | IOAP | IOAP⊆P_{I} | This defines IOAP as the set of OWL annotation properties. |
owl:OntologyProperty | C_{I} | IOXP | IOXP⊆P_{I} | This defines IOXP as the set of OWL ontology properties. |
owl:Ontology | C_{I} | IX | This defines IX as the set of OWL ontologies. | |
owl:AllDifferent | C_{I} | IAD | ||
rdf:List | IL | IL⊆R_{I} | This defines IL as the set of OWL lists. | |
rdf:nil | IL | |||
"l"^^d | CEXT_{I}(S_{I}(d)) | S_{I}("l"^^d) ∈ LV_{I} | Typed literals are well-behaved in OWL. |
OWL built-in syntactic classes and properties
I(owl:FunctionalProperty), I(owl:InverseFunctionalProperty), I(owl:SymmetricProperty), I(owl:TransitiveProperty), I(owl:DeprecatedClass), and I(owl:DeprecatedProperty) are in C_{I}.
I(owl:equivalentClass), I(owl:disjointWith), I(owl:equivalentProperty), I(owl:inverseOf), I(owl:sameAs), I(owl:differentFrom), I(owl:complementOf), I(owl:unionOf), I(owl:intersectionOf), I(owl:oneOf), I(owl:allValuesFrom), I(owl:onProperty), I(owl:someValuesFrom), I(owl:hasValue), I(owl:minCardinality), I(owl:maxCardinality), I(owl:cardinality), and I(owl:distinctMembers) are all in P_{I}.
I(owl:versionInfo), I(rdfs:label), I(rdfs:comment), I(rdfs:seeAlso), and I(rdfs:isDefinedBy) are all in IOAP. I(owl:imports), I(owl:priorVersion), I(owl:backwardCompatibleWith), and I(owl:incompatibleWith), are all in IOXP.
Characteristics of OWL classes, datatypes, and properties
If E is | then if e∈CEXT_{I}(S_{I}(E)) then | Note |
---|---|---|
owl:Class | CEXT_{I}(e)⊆IOT | Instances of OWL classes are OWL individuals. |
rdfs:Datatype | CEXT_{I}(e)⊆LV_{I} | |
owl:DataRange | CEXT_{I}(e)⊆LV_{I} | OWL dataranges are special kinds of datatypes. |
owl:ObjectProperty | EXT_{I}(e)⊆IOT×IOT | Values for indivdiual-valued properties are OWL individuals. |
owl:DatatypeProperty | EXT_{I}(e)⊆IOT×LV_{I} | Values for datatype properties are literal values. |
owl:AnnotationProperty | EXT_{I}(e)⊆IOT×(IOT∪LV_{I}) | Values for annotation properties are less unconstrained. |
owl:OntologyProperty | EXT_{I}(e)⊆IX×IX | Ontology properties relate ontologies to other ontologies. |
If E is | then c∈CEXT_{I}(S_{I}(E)) iff c∈IOOP∪IODP and | Note |
owl:FunctionalProperty | <x,y_{1}>, <x,y_{2}> ∈ EXT_{I}(c) implies y_{1} = y_{2} | Both individual-valued and datatype properties can be functional properties. |
If E is | then c∈CEXT_{I}(S_{I}(E)) iff c∈IOOP and | Note |
owl:InverseFunctionalProperty | <x_{1},y>, <x_{2},y>∈EXT_{I}(c) implies x_{1} = x_{2} | Only individual-valued properties can be inverse functional properties. |
owl:SymmetricProperty | <x,y> ∈ EXT_{I}(c) implies <y, x>∈EXT_{I}(c) | Only individual-valued properties can be symmetric properties. |
owl:TransitiveProperty | <x,y>, <y,z>∈EXT_{I}(c) implies <x,z>∈EXT_{I}(c) | Only individual-valued properties can be transitive properties. |
If-and-only-if conditions for rdfs:subClassOf, rdfs:subPropertyOf, rdfs:domain, and rdfs:range
If E is | then for | <x,y>∈EXT_{I}(S_{I}(E)) iff |
---|---|---|
rdfs:subClassOf | x,y∈IOC | CEXT_{I}(x) ⊆ CEXT_{I}(y) |
rdfs:subPropertyOf | x,y∈IOOP | EXT_{I}(x) ⊆ EXT_{I}(y) |
rdfs:subPropertyOf | x,y∈IODP | EXT_{I}(x) ⊆ EXT_{I}(y) |
rdfs:domain | x∈IOOP∪IODP,y∈IOC | <z,w>∈EXT_{I}(x) implies z∈CEXT_{I}(y) |
rdfs:range | x∈IOOP∪IODP,y∈IOC∪IDC | <w,z>∈EXT_{I}(x) implies z∈CEXT_{I}(y) |
Characteristics of OWL vocabulary related to equivalence
If E is | then <x,y>∈EXT_{I}(S_{I}(E)) iff |
---|---|
owl:equivalentClass | x,y∈IOC and CEXT_{I}(x)=CEXT_{I}(y) |
owl:disjointWith | x,y∈IOC and CEXT_{I}(x)∩CEXT_{I}(y)={} |
owl:equivalentProperty | x,y∈IOOP∪IODP and EXT_{I}(x) = EXT_{I}(y) |
owl:inverseOf | x,y∈IOOP and <u,v>∈EXT_{I}(x) iff <v,u>∈EXT_{I}(y) |
owl:sameAs | x = y |
owl:differentFrom | x ≠ y |
Conditions on OWL vocabulary related to boolean combinations and sets
We will say that l_{1} is a sequence of
y_{1},…,y_{n} over C iff
n=0 and l_{1}=S_{I}(rdf:nil)
or n>0 and l_{1}∈IL and
∃ l_{2}, …, l_{n} ∈ IL such that
<l_{1},y_{1}>∈EXT_{I}(S_{I}(rdf:first)), y_{1}∈C,
<l_{1},l_{2}>∈EXT_{I}(S_{I}(rdf:rest)), …,
<l_{n},y_{n}>∈EXT_{I}(S_{I}(rdf:first)), y_{n}∈C, and
<l_{n},S_{I}(rdf:nil)>∈EXT_{I}(S_{I}(rdf:rest)).
If E is | then <x,y>∈EXT_{I}(S_{I}(E)) iff |
---|---|
owl:complementOf | x,y∈ IOC and CEXT_{I}(x)=IOT-CEXT_{I}(y) |
owl:unionOf | x∈IOC and y is a sequence of y_{1},…y_{n} over IOC and CEXT_{I}(x) = CEXT_{I}(y_{1})∪…∪CEXT_{I}(y_{n}) |
owl:intersectionOf | x∈IOC and y is a sequence of y_{1},…y_{n} over IOC and CEXT_{I}(x) = CEXT_{I}(y_{1})∩…∩CEXT_{I}(y_{n}) |
owl:oneOf | x∈C_{I} and y is a sequence of y_{1},…y_{n} over IOT or over LV_{I} and CEXT_{I}(x) = {y_{1},..., y_{n}} |
Further conditions on owl:oneOf
If E is | and | then if <x,l>∈EXT_{I}(S_{I}(E)) then |
---|---|---|
owl:oneOf | l is a sequence of y_{1},…y_{n} over LV_{I} | x∈IDC |
owl:oneOf | l is a sequence of y_{1},…y_{n} over IOT | x∈IOC |
Conditions on OWL restrictions
If | then x∈IOR, y∈IOC∪IDC, p∈IOOP∪IODP, and CEXT_{I}(x) = |
---|---|
<x,y>∈EXT_{I}(S_{I}(owl:allValuesFrom))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) |
{u∈IOT | <u,v>∈EXT_{I}(p) implies v∈CEXT_{I}(y) } |
<x,y>∈EXT_{I}(S_{I}(owl:someValuesFrom))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) |
{u∈IOT | ∃ <u,v>∈EXT_{I}(p) such that v∈CEXT_{I}(y) } |
If | then x∈IOR, y∈IOT∪LV_{I}, p∈IOOP∪IODP, and CEXT_{I}(x) = |
<x,y>∈EXT_{I}(S_{I}(owl:hasValue))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) |
{u∈IOT | <u, y>∈EXT_{I}(p) } |
If | then x∈IOR, y∈LV_{I}, y is a non-negative integer, p∈IOOP∪IODP, and CEXT_{I}(x) = |
<x,y>∈EXT_{I}(S_{I}(owl:minCardinality))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) |
{u∈IOT | card({v ∈ IOT ∪ LV : <u,v>∈EXT_{I}(p)}) ≥ y } |
<x,y>∈EXT_{I}(S_{I}(owl:maxCardinality))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) |
{u∈IOT | card({v ∈ IOT ∪ LV : <u,v>∈EXT_{I}(p)}) ≤ y } |
<x,y>∈EXT_{I}(S_{I}(owl:cardinality))) ∧ <x,p>∈EXT_{I}(S_{I}(owl:onProperty))) |
{u∈IOT | card({v ∈ IOT ∪ LV : <u,v>∈EXT_{I}(p)}) = y } |
Comprehension conditions (principles)
The first two comprehension conditions require the existence of the finite sequences that are used in some OWL constructs. The third comprehension condition requires the existence of instances of owl:AllDifferent. The remaining comprehension conditions require the existence of the appropriate OWL descriptions and data ranges.
If there exists | then there exists l_{1},…,l_{n} ∈ IL with |
---|---|
x_{1}, …, x_{n} ∈ IOC | <l_{1},x_{1}> ∈ EXT_{I}(S_{I}(rdf:first)),
<l_{1},l_{2}> ∈ EXT_{I}(S_{I}(rdf:rest)), … <l_{n},x_{n}> ∈ EXT_{I}(S_{I}(rdf:first)), <l_{n},S_{I}(rdf:nil)> ∈ EXT_{I}(S_{I}(rdf:rest)) |
x_{1}, …, x_{n} ∈ IOT∪LV_{I} | <l_{1},x_{1}> ∈ EXT_{I}(S_{I}(rdf:first)),
<l_{1},l_{2}> ∈ EXT_{I}(S_{I}(rdf:rest)), … <l_{n},x_{n}> ∈ EXT_{I}(S_{I}(rdf:first)), <l_{n},S_{I}(rdf:nil)> ∈ EXT_{I}(S_{I}(rdf:rest)) |
If there exists | then there exists y with |
l, a sequence of x_{1},…,x_{n} over IOT with x_{i}≠x_{j} for 1≤i<j≤n |
y∈IAD, <y,l>∈EXT_{I}(S_{I}(owl:distinctMembers)) |
If there exists | then there exists y with |
l, a sequence of x_{1},…,x_{n} over IOC | y∈IOC, <y,l> ∈ EXT_{I}(S_{I}(owl:unionOf)) |
l, a sequence of x_{1},…,x_{n} over IOC | y∈IOC, <y,l> ∈ EXT_{I}(S_{I}(owl:intersectionOf)) |
l, a sequence of x_{1},…,x_{n} over IOT | y∈IOC, <y,l> ∈ EXT_{I}(S_{I}(owl:oneOf)) |
l, a sequence of x_{1},…,x_{n} over LV_{I} | y∈IDC, <y,l> ∈ EXT_{I}(S_{I}(owl:oneOf)) |
If there exists | then there exists y ∈ IOC with |
x ∈ IOC | <y,x> ∈ EXT_{I}(S_{I}(owl:complementOf)) |
If there exists | then there exists y ∈ IOR with |
x ∈ IOOP∪IODP ∧ w ∈ IOC ∪ IDC | <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:allValuesFrom)) |
x ∈ IOOP∪IODP ∧ w ∈ IOC ∪ IDC | <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:someValuesFrom)) |
x ∈ IOOP∪IODP ∧ w ∈ IOT ∪ LV_{I} | <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:hasValue)) |
x ∈ IOOP∪IODP ∧ w ∈ LV_{I} ∧ w is a non-negative integer | <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:minCardinality)) |
x ∈ IOOP∪IODP ∧ w ∈ LV_{I} ∧ w is a non-negative integer | <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:maxCardinality)) |
x ∈ IOOP∪IODP ∧ w ∈ LV_{I} ∧ w is a non-negative integer | <y,x> ∈ EXT_{I}(S_{I}(owl:onProperty)) ∧ <y,w> ∈ EXT_{I}(S_{I}(owl:cardinality)) |
OWL Full augments the common conditions with conditions that force the parts of the OWL universe to be the same as their analogues in RDF. These new conditions strongly interact with the common conditions. For example, because in OWL Full IOT is the entire RDF domain of discourse, the second comprehension condition for lists generates lists of any kind, including lists of lists.
Definition: A OWL Full interpretation of a vocabulary V is an OWL interpretation as above that satisfies the following conditions.
IOT = R_{I} |
IOOP = P_{I} |
IOC = C_{I} |
Definition: Let K be a collection of RDF graphs. K is imports closed iff for every triple in any element of K of the form x owl:imports u . then K contains a graph that is the result of the RDF processing of the RDF/XML document, if any, accessible at u into an RDF graph. The imports closure of a collection of RDF graphs is the smallest import-closed collection of RDF graphs containing the graphs.
Definitions: Let K and Q be collections of RDF graphs. Then K OWL Full entails Q iff every OWL Full interpretation (of any vocabulary V that includes the RDF and RDFS vocabularies and the OWL vocabulary) that satisfies all the RDF graphs in K also satisfies all the RDF graphs in Q. K is OWL Full consistent iff there is some OWL Full interpretation that satisfies all the RDF graphs in K.
OWL DL augments the above conditions with a separation of the domain of discourse into several disjoint parts. This separation has two consequences. First, the OWL portion of the domain of discourse becomes standard first-order, in that predicates (classes and properties) and individuals are disjoint. Second, the OWL portion of a OWL DL interpretation can be viewed as a Description Logic interpretation for a particular expressive Description Logic.
Definition: A OWL DL interpretation of a vocabulary V is an OWL interpretation as above that satisfies the following conditions.
LV_{I}, IOT, IOC, IDC, IOOP, IODP, IOAP, IOXP, IL, and IX are all pairwise disjoint. |
For v in the disallowed vocabulary (Section 4.2), S_{I}(v) ∈ R_{I} - (LV_{I}∪IOT∪IOC∪IDC∪IOOP∪IODP∪IOAP∪IOXP∪IL∪IX). |
Entailment in OWL DL is defined similarly to entailment in OWL Full.
Definitions: Let K and Q be collections of RDF graphs. Then K OWL DL entails Q iff every OWL DL interpretation (of any vocabulary V that includes the RDF and RDFS vocabularies and the OWL vocabulary) that satisfies all the RDF graphs in K also satisfies all the RDF graphs in Q. K is OWL DL consistent iff there is some OWL DL interpretation that satisfies all the RDF graphs in K.
There is a strong correspondence between the direct semantics and the OWL DL semantics. Basically, an ontology that could be written in the abstract syntax OWL DL entails another exactly when it entails the other in the direct semantics. There are a number of complications to this basic story having to do with splitting up the vocabulary so that, for example, concepts, properties, and individuals do not interfere, and arranging that imports works the same.
For the correspondence to be valid there has to be some connection between an ontology in the abstract syntax with a particular name and the document available on the Web at that URI. This connection is outside the semantics here, and so must be specially arranged. This connection is also only an idealization of the Web, as it ignores temporal and transport aspects of the Web.
Definition: Let T be the mapping from OWL ontologies in the abstract syntax to RDF graphs from Section 4.1. Let O be a collection of OWL DL ontologies in abstract syntax form. O is said to be imports closed iff for any URI, u, in an imports directive in any ontology in O the RDF parsing of the document accessible on the Web at u results in T(K), where K is the ontology in O with name u.
Theorem 1:
Let O and O' be collections of OWL DL ontologies in abstract syntax form
that are imports closed,
such that their union has a
separated vocabulary
(Section 4.2).
Then
O entails O'
if and only if
the translation (Section 4.1) of the ontologies in O
OWL DL entails
the translation of the ontologies in O'.
The proof is contained in Appendix A.1.
A simple corollary of this is that O is consistent if and only if the translation of the ontologies in O is consistent.
There is also a correspondence between OWL DL entailment and OWL Full entailment.
Theorem 2: Let O and O' be collections of OWL DL ontologies in abstract syntax form that are imports closed, such that their union has a separated vocabulary (Section 4.2). Then the translation of the ontologies in O OWL Full entails the translation of the ontologies in O' if the translation of the ontologies in O OWL DL entails the translation of the ontologies in O'. A sketch of the proof is contained in Appendix A.2.