OWL Web Ontology Language
Semantics and Abstract Syntax
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

Please refer to the errata for this document, which may include some normative corrections.

See also translations.


Contents


3. Direct Model-Theoretic Semantics (Normative)

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, which 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 and literals in that ontology, as well as ontologies that are imported by the ontology, but can include other URI references and literals as well.

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

Definition: An OWL vocabulary V consists of a set of literals VL and seven sets of URI references, VC, VD, VI, VDP, VIP, VAP, and VO. In any vocabulary VC and VD are disjoint and VDP, VIP, VAP, and VOP are pairwise disjoint. VC, the class names of a vocabulary, contains owl:Thing and owl:Nothing. VD, the datatype names of a vocabulary, contains the URI references for the built-in OWL datatypes and rdfs:Literal. VAP, the annotation property names of a vocabulary, contains owl:versionInfo, rdfs:label, rdfs:comment, rdfs:seeAlso, and rdfs:isDefinedBy. VIP, the individual-valued property names of a vocabulary, VDP, the data-valued property names of a vocabulary, and VI, the individual names of a vocabulary, VO, the ontology names of a vocabulary, do not have any required members.

Definition: As in RDF, a datatype d is characterized by a lexical space, L(d), which is a set of Unicode strings; a value space, V(d); and a total mapping L2V(d) from the lexical space to the value space.

Definition: A datatype map D is a partial mapping from URI references to datatypes that maps xsd:string and xsd:integer to the appropriate XML Schema datatypes.

A datatype map may contain datatypes for the other built-in OWL datatypes. It may also contain other datatypes, but there is no provision in the OWL syntax for conveying what these datatypes are.

Definition: Let D be a datatype map. An Abstract OWL interpretation with respect to D with vocabulary VL, VC, VD, VI, VDP, VIP, VAP, VO is a tuple of the form: I = <R, EC, ER, L, S, LV> where (with P being the power set operator)

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. (The property rdf:type is added to the annotation properties so as to provide a meaning for deprecation, see below.)'' 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 in VL 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, values, and annotations as in the EC Extension Table.

EC Extension Table
Abstract SyntaxInterpretation (value of EC)
complementOf(c) O - EC(c)
unionOf(c1 … cn) EC(c1) ∪ … ∪ EC(cn)
intersectionOf(c1 … cn) EC(c1) ∩ … ∩ EC(cn)
oneOf(i1 … in), for ij individual IDs {S(i1), …, S(in)}
oneOf(v1 … vn), for vj literals {S(v1), …, S(vn)}
restriction(p x1 … xn), for n > 1 EC(restriction(p x1)) ∩…∩EC(restriction(p xn))
restriction(p allValuesFrom(r)) {x ∈ O | <x,y> ∈ ER(p) implies y ∈ EC(r)}
restriction(p someValuesFrom(e)) {x ∈ O | ∃ <x,y> ∈ ER(p) ∧ y ∈ EC(e)}
restriction(p value(i)), for i an individual ID {x ∈ O | <x,S(i)> ∈ ER(p)}
restriction(p value(v)), for v a literal {x ∈ O | <x,S(v)> ∈ ER(p)}
restriction(p minCardinality(n)) {x ∈ O | card({y ∈ O∪LV : <x,y> ∈ ER(p)}) ≥ n}
restriction(p maxCardinality(n)) {x ∈ O | card({y ∈ O∪LV : <x,y> ∈ ER(p)}) ≤ n}
restriction(p cardinality(n)) {x ∈ O | card({y ∈ O∪LV : <x,y> ∈ ER(p)}) = n}
Individual(annotation(p1 o1)annotation(pk ok)
    type(c1)type(cm) pv1 … pvn)
EC(annotation(p1 o1)) ∩ … EC(annotation(pk ok)) ∩
EC(c1) ∩ … ∩ EC(cm) ∩ EC(pv1) ∩…∩ EC(pvn)
Individual(i annotation(p1 o1)annotation(pk ok)
    type(c1)type(cm) pv1 … pvn)
{S(i)} ∩ EC(annotation(p1 o1)) ∩ … EC(annotation(pk ok)) ∩
EC(c1) ∩ … ∩ EC(cm) ∩ EC(pv1) ∩…∩ EC(pvn)
value(p Individual()) {x ∈ O | ∃ y∈EC(Individual()) : <x,y> ∈ ER(p)}
value(p id) for id an individual ID {x ∈ O | <x,S(id)> ∈ ER(p) }
value(p v) for v a literal {x ∈ O | <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
DirectiveConditions on interpretations
Class(c [Deprecated] complete
    annotation(p1 o1)annotation(pk ok)
    descr1 … descrn)
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ]
S(c) ∈ EC(annotation(p1 o1)) … S(c) ∈ EC(annotation(pk ok))
EC(c) = EC(descr1) ∩…∩ EC(descrn)
Class(c [Deprecated] partial
    annotation(p1 o1)annotation(pk ok)
    descr1 … descrn)
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ]
S(c) ∈ EC(annotation(p1 o1)) … S(c) ∈ EC(annotation(pk ok))
EC(c) ⊆ EC(descr1) ∩…∩ EC(descrn)
EnumeratedClass(c [Deprecated]
    annotation(p1 o1)annotation(pk ok)
    i1 … in)
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ]
S(c) ∈ EC(annotation(p1 o1)) … S(c) ∈ EC(annotation(pk ok))
EC(c) = { S(i1), …, S(in) }
Datatype(c [Deprecated]
    annotation(p1 o1)annotation(pk ok) )
[ <S(c),S(owl:DeprecatedClass)> ∈ ER(rdf:type) ]
S(c) ∈ EC(annotation(p1 o1)) … S(c) ∈ EC(annotation(pk ok))
EC(c) ⊆ LV
DisjointClasses(d1 … dn) EC(di) ∩ EC(dj) = { } for 1 ≤ i < j ≤ n
EquivalentClasses(d1 … dn) EC(di) = EC(dj) for 1 ≤ i < j ≤ n
SubClassOf(d1 d2) EC(d1) ⊆ EC(d2)
DatatypeProperty(p [Deprecated]
    annotation(p1 o1)annotation(pk ok)
    super(s1)super(sn)
    domain(d1)domain(dn) range(r1)range(rn)
    [Functional])
[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type) ]
S(p) ∈ EC(annotation(p1 o1)) … S(p) ∈ EC(annotation(pk ok))
ER(p) ⊆ O×LV ∩ ER(s1) ∩…∩ ER(sn) ∩
       EC(d1)×LV ∩…∩ EC(dn)×LV ∩ O×EC(r1) ∩…∩ O×EC(rn)
[ER(p) is functional]
ObjectProperty(p [Deprecated]
    annotation(p1 o1)annotation(pk ok)
    super(s1)super(sn)
   
domain(d1)domain(dn) range(r1)range(rn)
   
[inverse(i)] [Symmetric]
    [
Functional] [ InverseFunctional]
    [
Transitive])
[ <S(c),S(owl:DeprecatedProperty)> ∈ ER(rdf:type)]
S(p) ∈ EC(annotation(p1 o1)) … S(p) ∈ EC(annotation(pk ok))
ER(p) ⊆ O×O ∩ ER(s1) ∩…∩ ER(sn) ∩
        EC(d1O ∩…∩ EC(dnOO×EC(r1) ∩…∩ O×EC(rn)
[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(p1 o1)annotation(pk ok)) S(p) ∈ EC(annotation(p1 o1)) … S(p) ∈ EC(annotation(pk ok))
OntologyProperty(p annotation(p1 o1)annotation(pk ok)) S(p) ∈ EC(annotation(p1 o1)) … S(p) ∈ EC(annotation(pk ok))
EquivalentProperties(p1 … pn) ER(pi) = ER(pj) for 1 ≤ i < j ≤ n
SubPropertyOf(p1 p2) ER(p1) ⊆ ER(p2)
SameIndividual(i1 … in) S(ij) = S(ik) for 1 ≤ j < k ≤ n
DifferentIndividuals(i1 … in) S(ij) ≠ S(ik) for 1 ≤ j < k ≤ n
Individual([i] annotation(p1 o1)annotation(pk ok)
   type(c1)type(cm) pv1 … pvn)
EC(Individual([i] annotation(p1 o1)annotation(pk ok)
   type(c1)type(cm) pv1 … pvn)) is nonempty

3.4. Interpreting Ontologies

From Section 2, an OWL ontology can have annotations, which need their own semantic conditions. 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 D be a datatype map. An Abstract OWL interpretation, I, with respect to D with vocabulary consisting of VL, VC, VD, VI, VDP, VIP, VAP, VO, satisfies an OWL ontology, O, iff

  1. 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 VC (VD, VI, VDP, VIP, VAP, VO, respectively);
  2. each literal in O belongs to VL;
  3. I satisfies each directive in O, except for Ontology Annotations;
  4. there is some o ∈ R with <o,S(owl:Ontology)> ∈ ER(rdf:type) such that for each Ontology Annotation of the form Annotation(p v), <o,S(v)> ∈ ER(p) and that if O has name n, then S(n) = o; and
  5. I satisfies each ontology mentioned in an owl:imports annotation directive of O.

Definition: A collection of abstract OWL ontologies and axioms and facts is consistent with respect to datatype map D iff there is some interpretation I with respect to D such that I satisfies each ontology and axiom and fact in the collection.

Definition: A collection O of abstract OWL ontologies and axioms and facts entails an abstract OWL ontology or axiom or fact O' with respect to a datatype map D if each interpretation with respect to map D that satisfies each ontology and axiom and fact in O also satisfies O'.