Web Ontology Language (OWL) Abstract Syntax and Semantics
Section 3. Direct Model-Theoretic Semantics

Editors:: Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies
Ian Horrocks, Department of Computer Science, University of Manchester

3. Direct Model-Theoretic Semantics

This model-theoretic semantics for OWL goes directly from ontologies in the OWL DL abstract syntax, which includes the OWL Lite abstract syntax, to a standard model theory. It is simpler than the semantics in Section 5 for RDF graphs that is a vocabulary extension of the RDFS semantics.

3.1. Vocabularies and Interpretations

The semantics here starts with the notion of a vocabulary. When considering an OWL ontology, the vocabulary must include all the URI references in that ontology, as well as ontologies that are imported by the ontology, but can include other URI references as well.

In this section V_OP will be the URI references for the built-in OWL ontology properties.

Definition: An OWL vocabulary V consists of seven sets of URI references, V_C, V_D, V_I, V_DP, V_IP, V_AP, and V_O. In any vocabulary V_C and V_D are disjoint and V_DP, V_IP, V_AP, and V_OP are pairwise disjoint. V_C, the class names of a vocabulary, contains owl:Thing and owl:Nothing. V_D, the datatype names of a vocabulary, contains the URI references for the built-in OWL datatypes and rdfs:Literal. V_AP, the annotation property names of a vocabulary, contains owl:versionInfo, rdfs:label, rdfs:comment, rdfs:seeAlso, and rdfs:isDefinedBy. V_IP, the individual-valued property names of a vocabulary, V_DP, the data-valued property names of a vocabulary, and V_I, the individual names of a vocabulary, V_O, the ontology names of a vocabulary, do not have any required members.

Definition: A datatype theory is a six-tuple < D, LV, N, L, V, L2V > where D is a set of datatypes, LV is a set of data values, N is a partial map from URI references to D, L maps D to sets of strings, V maps D to sets of elements of LV, and L2V maps each d in D to a map from L(d) to V(d). LV always contains the (non-disjoint) union of the set of Unicode strings and the set of pairs consisting of Unicode strings and language tags.

Definition: Let T = < D_T, LV_T, N_T, L_T, V_T, L2V_T > be a datatype theory. An Abstract OWL interpretation with respect to T with vocabulary V_C, V_D, V_I, V_DP, V_IP, V_AP, V_O is a tuple of the form: I = <R, EC, ER, L, S> where (with P being the power set operator)

R, the resources of I, is a non-empty set, disjoint from LV_T

EC : V_C → P(R)

EC : V_D → P(LV_T)

ER : V_DP → P(R×LV_T)

ER : V_IP → P(R×R)

ER : V_AP ∪ { rdf:type } → P(R×(R∪LV_T))

ER : V_OP → P(R×R)

L : TL → LV_T, where TL is the set of typed literals

S : V_I ∪ V_C ∪ V_D ∪ V_DP ∪ V_IP ∪ V_AP ∪ V_O ∪ { owl:DeprecatedClass, owl:DeprecatedProperty } → R

EC(owl:Thing) = R

EC(owl:Nothing) = { }

EC(rdfs:Literal) = LV_T

If N_T(d') is defined then EC(d') = V_T(N_T(d'))

If N_T(d') is defined then L("l"^^d') ∈ V_T(N_T(d'))

If N_T(d') is defined and l ∈ L_T(N_T(d')) then L("l"^^d') = L2V_T(N_T(d'))(l)

If N_T(d') is defined and l ∉ L_T(N_T(d')) then L("l"^^d') ∈ R - V_T(N_T(d'))

EC provides meaning for URI references that are used as OWL classes and datatypes. ER provides meaning for URI references that are used as OWL properties. L provides meaning for typed literals. S provides meaning for URI references that are used to denote OWL individuals, and helps provide meaning for annotations. Note that there are no interpretations that can satisfy all the requirements placed on badly-formed literals, i.e., one whose lexical form is invalid for the datatype, such as 1.5^^xsd:integer.

S is extended to plain literals by (essentially) mapping them onto themselves, i.e., S("l") = l for l a plain literal without a language tag and S("l"@t) = <l,t> for l a plain literal with a language tag. S is extended to typed literals by using L, S(l) = L(l) for l a typed literal.

3.2. Interpreting Embedded Constructs

EC is extended to the syntactic constructs of descriptions, data ranges, individuals, and values as in the EC Extension Table.

EC Extension Table
Abstract Syntax	Interpretation (value of EC)
complementOf(c)	R - EC(c)
unionOf(c₁ … c_n)	EC(c₁) ∪ … ∪ EC(c_n)
intersectionOf(c₁ … c_n)	EC(c₁) ∩ … ∩ EC(c_n)
oneOf(i₁ … i_n), for i_j individual IDs	{S(i₁), …, S(i_n)}
oneOf(v₁ … v_n), for v_j literals	{S(v₁), …, S(v_n)}
restriction(p x₁ … x_n)	EC(restriction(p x₁)) ∩…∩EC(restriction(p x_n))
restriction(p allValuesFrom(r))	{x ∈ R \| <x,y> ∈ ER(p) implies y ∈ EC(r)}
restriction(p someValuesFrom(e))	{x ∈ R \| ∃ <x,y> ∈ ER(p) ∧ y ∈ EC(e)}
restriction(p value(i)), for i an individual ID	{x ∈ R \| <x,S(i)> ∈ ER(p)}
restriction(p value(v)), for v a literal	{x ∈ R \| <x,S(v)> ∈ ER(p)}
restriction(p minCardinality(n))	{x ∈ R \| card({y ∈ R∪LV : <x,y> ∈ ER(p)}) ≥ n}
restriction(p maxCardinality(n))	{x ∈ R \| card({y ∈ R∪LV : <x,y> ∈ ER(p)}) ≤ n}
restriction(p cardinality(n))	{x ∈ R \| card({y ∈ R∪LV : <x,y> ∈ ER(p)}) = n}
Individual(annotation(p₁ o₁) … annotation(p_k o_k) type(c₁) … type(c_m) pv₁ … pv_n)	EC(annotation(p₁ o₁)) ∩ … EC(annotation(p_k o_k)) ∩ EC(c₁) ∩ … ∩ EC(c_m) ∩ EC(pv₁) ∩…∩ EC(pv_n)
Individual(i annotation(p₁ o₁) … annotation(p_k o_k) type(c₁) … type(c_m) pv₁ … pv_n)	{S(i)} ∩ EC(annotation(p₁ o₁)) ∩ … EC(annotation(p_k o_k)) ∩ EC(c₁) ∩ … ∩ EC(c_m) ∩ EC(pv₁) ∩…∩ EC(pv_n)
value(p Individual(…))	{x ∈ R \| ∃ y∈EC(Individual(…)) : <x,y> ∈ ER(p)}
value(p id) for id an individual ID	{x ∈ R \| <x,S(id)> ∈ ER(p) }
value(p v) for v a literal	{x ∈ R \| <x,S(v)> ∈ ER(p) }
annotation(p o) for o a URI reference	{x ∈ R \| <x,S(o)> ∈ ER(p) }
annotation(p Individual(…))	{x ∈ R \| ∃ y ∈ EC(Individual(…)) : <x,y> ∈ ER(p) }

3.3. Interpreting Axioms and Facts

An Abstract OWL interpretation, I, satisfies OWL axioms and facts as given in Axiom and Fact Interpretation Table. In the table, optional parts of axioms and facts are given in square brackets ([…]) and have corresponding optional conditions, also given in square brackets.

Interpretation of Axioms and Facts
Directive	Conditions on interpretations
Class(c [Deprecated] complete annotation(p₁ o₁) … annotation(p_k o_k) descr₁ … descr_n)	[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p₁ o₁)) … S(c) ∈ EC(annotation(p_k o_k)) EC(c) = EC(descr₁) ∩…∩ EC(descr_n)
Class(c [Deprecated] partial annotation(p₁ o₁) … annotation(p_k o_k) descr₁ … descr_n)	[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p₁ o₁)) … S(c) ∈ EC(annotation(p_k o_k)) EC(c) ⊆ EC(descr₁) ∩…∩ EC(descr_n)
EnumeratedClass(c [Deprecated] annotation(p₁ o₁) … annotation(p_k o_k) i₁ … i_n)	[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p₁ o₁)) … S(c) ∈ EC(annotation(p_k o_k)) EC(c) = { S(i₁), …, S(i_n) }
Datatype(c [Deprecated] annotation(p₁ o₁) … annotation(p_k o_k) )	[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ] S(c) ∈ EC(annotation(p₁ o₁)) … S(c) ∈ EC(annotation(p_k o_k)) EC(c) ⊆ LV_T
DisjointClasses(d₁ … d_n)	EC(d_i) ∩ EC(d_j) = { } for 1 ≤ i < j ≤ n
EquivalentClasses(d₁ … d_n)	EC(d_i) = EC(d_j) for 1 ≤ i < j ≤ n
SubClassOf(d₁ d₂)	EC(d₁) ⊆ EC(d₂)
DatatypeProperty(p [Deprecated] annotation(p₁ o₁) … annotation(p_k o_k) super(s₁) … super(s_n) domain(d₁) … domain(d_n) range(r₁) … range(r_n) [Functional])	[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type) ] S(p) ∈ EC(annotation(p₁ o₁)) … S(p) ∈ EC(annotation(p_k o_k)) ER(p) ⊆ R×LV ∩ ER(s₁) ∩…∩ ER(s_n) ∩ EC(d₁)×LV ∩…∩ EC(d_n)×LV ∩ R×EC(r₁) ∩…∩ R×EC(r_n) [ER(p) is functional]
ObjectProperty(p [Deprecated] annotation(p₁ o₁) … annotation(p_k o_k) super(s₁) … super(s_n) domain(d₁) … domain(d_n) range(r₁) … range(r_n) [inverse(i)] [Symmetric] [Functional] [ InverseFunctional] [Transitive])	[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type)] S(p) ∈ EC(annotation(p₁ o₁)) … S(p) ∈ EC(annotation(p_k o_k)) ER(p) ⊆ R×R ∩ ER(s₁) ∩…∩ ER(s_n) ∩ EC(d₁)×R ∩…∩ EC(d_n)×R ∩ R×EC(r₁) ∩…∩ R×EC(r_n) [ER(p) is the inverse of ER(i)] [ER(p) is symmetric] [ER(p) is functional] [ER(p) is inverse functional] [ER(p) is transitive]
AnnotationProperty(p annotation(p₁ o₁) … annotation(p_k o_k))	S(p) ∈ EC(annotation(p₁ o₁)) … S(p) ∈ EC(annotation(p_k o_k))
EquivalentProperties(p₁ … p_n)	ER(p_i) = ER(p_j) for 1 ≤ i < j ≤ n
SubPropertyOf(p₁ p₂)	ER(p₁) ⊆ ER(p₂)
SameIndividual(i₁ … i_n)	S(i_j) = S(i_k) for 1 ≤ j < k ≤ n
DifferentIndividuals(i₁ … i_n)	S(i_j) ≠ S(i_k) for 1 ≤ j < k ≤ n
Individual([i] annotation(p₁ o₁) … annotation(p_k o_k) type(c₁) … type(c_m) pv₁ … pv_n)	EC(Individual([i] annotation(p₁ o₁) … annotation(p_k o_k) type(c₁) … type(c_m) pv₁ … pv_n)) is nonempty

3.4. Interpreting Ontologies

From Section 2, an OWL ontology can have annotations. These components of an OWL ontology have their own semantic conditions, as given in the Annotation and Fact Interpretation Table.

Local Interpretation of Annotations
Directive	Conditions on interpretations for Ontology with name u
Annotation(p o)	<S(u),S(o)> ∈ ER(p)
Directive	Conditions on interpretations for Unnamed Ontology
Annotation(p o)	∃x ∈ R <x,S(o)> ∈ ER(p)

Aside from this local meaning, an owl:imports annotation also imports the contents of another OWL ontology into the current ontology. The imported ontology is the one, if any, that has as name the argument of the imports construct. (This treatment of imports is divorced from Web issues. The intended use of names for OWL ontologies is to make the name be the location of the ontology on the Web, but this is outside of this formal treatment.)

Definition: Let T be a datatype theory. An Abstract OWL interpretation, I, with respect to T with vocabulary consisting of V_C, V_D, V_I, V_DP, V_IP, V_AP, V_O, satisfies an OWL ontology, O, iff

each URI reference in O used as a class ID (datatype ID, individual ID, data-valued property ID, individual-valued property ID, annotation property ID, annotation ID, ontology ID) belongs to V_C (V_D, V_I, V_DP, V_IP, V_AP, V_O, respectively);

I satisfies each directive in O; and

I satisfies each ontology mentioned in an owl:imports annotation directive of O.

Definition: An Abstract OWL ontology is consistent with respect to datatype theory T if there is some interpretation I with respect to T such that I satisfies the ontology.

Definition: A collection of abstract OWL ontologies entails an OWL axiom or fact with respect to a datatype theory T if each interpretation with respect to T that satisfies each of the ontologies also satisfies the axiom or fact. A collection of abstract OWL ontologies entails an abstract OWL ontology with respect to a datatype theory T if each interpretation with respect to T that satisfies each ontology in the collection also satisfies the ontology.

Web Ontology Language (OWL) Abstract Syntax and Semantics Section 3. Direct Model-Theoretic Semantics