OWL 2 Web Ontology Language:
Model-Theoretic Semantics

W3C Editor's Draft 11 April 2008

This version:: http://www.w3.org/2007/OWL/draft/ED-owl2-semantics-20080411/
Latest editor's draft:: http://www.w3.org/2007/OWL/draft/owl2-semantics/
Previous version:: http://www.w3.org/2007/OWL/draft/WD-owl11-semantics-20080108/ (color-coded diff)

Authors:: Bernardo Cuenca Grau, Oxford University; Boris Motik, Oxford University
Contributors:: Ian Horrocks, Oxford University; Bijan Parsia, The University of Manchester; Peter F. Patel-Schneider, Bell Labs Research, Alcatel-Lucent; Ulrike Sattler, The University of Manchester

Abstract

OWL 2 extends the W3C OWL Web Ontology Language with a small but useful set of features that have been requested by users, for which effective reasoning algorithms are now available, and that OWL tool developers are willing to support. The new features include extra syntactic sugar, additional property and qualified cardinality constructors, extended datatype support, simple metamodeling, and extended annotations. This document provides a model-theoretic semantics for OWL 2.

Status of this Document

May Be Superseded

This section describes the status of this document at the time of its publication. Other documents may supersede this document. A list of current W3C publications and the latest revision of this technical report can be found in the W3C technical reports index at http://www.w3.org/TR/.

This document is being published as one of a set of 6 documents:

Structural Specification and Functional-Style Syntax
Model-Theoretic Semantics (this document)
Mapping to RDF Graphs
XML Serialization
Profiles
Primer

Summary of Changes

Since the previous Working Draft (dated 8 January 2008), the only change is the name of the language, from "OWL 1.1" to "OWL 2". Since the group is publishing three new Working Drafts, and the name has changed, it decided to publish the complete set with consistent names.

Please Comment By 11 May 2008

The OWL Working Group seeks public feedback on these Working Drafts. Please send your comments to public-owl-comments@w3.org (public archive). If possible, please offer specific changes to the text that would address your concern. You may also wish to check the Wiki Version of this document for internal-review comments and changes being drafted which may address your concerns.

No Endorsement

Publication as a Working Draft does not imply endorsement by the W3C Membership. This is a draft document and may be updated, replaced or obsoleted by other documents at any time. It is inappropriate to cite this document as other than work in progress.

Patents

This document was produced by a group operating under the 5 February 2004 W3C Patent Policy. W3C maintains a public list of any patent disclosures made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent. An individual who has actual knowledge of a patent which the individual believes contains Essential Claim(s) must disclose the information in accordance with section 6 of the W3C Patent Policy.

1 Introduction
2 Model-Theoretic Semantics for OWL 2
3 References

1 Introduction

Editor's Note: See Issue-72 (Annotation Semantics).

Editor's Note: See Issue 63 (OWL Full Semantics).

Editor's Note: See Issue 69 (punning).

This document defines the formal semantics of OWL 2. The semantics given here follows the principles for defining the semantics of description logics [Description Logics] and is compatible with the description logic SROIQ presented in [SROIQ]. Unfortunately, the definition of SROIQ given in [SROIQ] does not provide for datatypes and metamodeling. Therefore, the semantics of OWL 2 is defined in a direct model-theoretic way, by interpreting the constructs of the functional-style syntax from [OWL 2 Specification]. For the constructs available in SROIQ, the semantics of SROIQ trivially corresponds to the one defined in this document.

OWL 2 does not have an RDF-compatible semantics. Ontologies expressed in OWL RDF are given semantics by converting then into the functional-style syntax and interpreting the result as specified in this document.

OWL 2 allows for annotations of ontologies and ontology entities (classes, properties, and individuals) and ontology axioms. Annotations, however, have no semantic meaning in OWL 2 and are ignored in this document. Definitions in OWL 2 similarly have no semantics. Constructs only used in annotations and definitions, like ObjectProperty, therefore do not show up in this document.

Since OWL 2 is an extension of OWL DL, this document also provides a formal semantics for OWL Lite and OWL DL and it is equivalent to the definition given in [OWL Abstract Syntax and Semantics].

2 Model-Theoretic Semantics for OWL 2

Editor's Note: See Issue-73 (infinite universe ).

A vocabulary (or signature) V = ( N_C , N_Po , N_Pd , N_I , N_D , N_V ) is a 6-tuple where

N_C is a set of OWL classes,
N_Po is a set of object properties,
N_Pd is a set of data properties,
N_I is a set of individuals, and
N_D is a set of datatypes each associated with a positive integer datatype arity,
N_V is a set of well-formed constants.

Since OWL 2 allows punning [Metamodeling] in the signature, we do not require the sets N_C , N_Po , N_Pd , N_I , N_D , and N_V to be pair-wise disjoint. Thus, the same name can be used in an ontology to denote a class, a datatype, a property (object or data), an individual, and a constant. The set N_D is defined as it is because a datatype is defined by its name and the arity, and such a definition allows one to reuse the same name with different arities.

The semantics of OWL 2 is defined with respect to a concrete domain, which is a tuple D = ( Δ_D , .^D ) where

Δ_D is a fixed set called the data domain,
.^D assigns to each constant v ∈ N_V an element v^D of Δ_D, and
.^D assigns to each datatype d ∈ N_D with arity n an n-ary relation d^D over Δ_D.

The set of datatypes N_D in each OWL 2 vocabulary must include a unary datatype rdfs:Literal interpreted as Δ_D; furthermore, it must also include the following unary datatypes: xsd:string, xsd:boolean, xsd:decimal, xsd:float, xsd:double, xsd:dateTime, xsd:time, xsd:date, xsd:gYearMonth, xsd:gYear, xsd:gMonthDay, xsd:gDay, xsd:gMonth, xsd:hexBinary, xsd:base64Binary, xsd:anyURI, xsd:normalizedString, xsd:token, xsd:language, xsd:NMTOKEN, xsd:Name, xsd:NCName, xsd:integer, xsd:nonPositiveInteger, xsd:negativeInteger, xsd:long, xsd:int, xsd:short, xsd:byte, xsd:nonNegativeInteger, xsd:unsignedLong, xsd:unsignedInt, xsd:unsignedShort, xsd:unsignedByte, and xsd:positiveInteger. These datatypes, as well as the well-formed constants from N_V, are interpreted as specified in [XML Schema Datatypes]. (Note that the value spaces of primitive XML Schema Datatypes are disjoint, so "2"^^xsd:decimal^D is different from "2"^^xsd:float"^D.)

The set Δ_D is a fixed set that must be large enough; that is, it must contain the extension of each datatype from N_D and, apart from that, an infinite number of other objects. Such a definition is ambiguous, as it does not uniquely single out a particular set Δ_D; however, the choice of the actual set is not actually relevant for the definition of the semantics, as long as it contains the interpretations of all datatypes that one can "reasonably think of." This allows the implementations to support datatypes other than the ones mentioned in the previous paragraphs without affecting the semantics.

Given a vocabulary V and a concrete domain D, an interpretation I = ( Δ_I , .^Ic , .^Ipo , .^Ipd , .^Ii ) is a 5-tuple where

Δ_I is a nonempty set disjoint with Δ_D, called the object domain;
.^Ic is the class interpretation function that assigns to each OWL class A ∈ N_Ic a subset A^Ic of Δ_I ;
.^Ipo is the object property interpretation function that assigns to each object property R ∈ N_Po a subset R^Ipo of Δ_I x Δ_I ;
.^Ipd is the data property interpretation function that assigns to each data property U ∈ N_Pd a subset U^Ipd of Δ_I x Δ_D ;
.^Ii is the individual interpretation function that assigns to each individual a ∈ N_I an element a^Ii from Δ_I.

We extend the object interpretation function .^Ipo to object property expressions as shown in Table 1.

Table 1. Interpreting Object Property Expressions
Object Property Expression	Interpretation
InverseObjectProperty(R)	{ ( x , y ) \| ( y , x ) ∈ R^Ipo }

We extend the interpretation function .^D to data ranges as shown in Table 2.

Table 2. Interpreting Data Ranges
Data Range	Interpretation
DataOneOf(v₁ ... v_n)	{ v₁^D , ... , v_n^D }
DataComplementOf(DR)	( Δ_D )ⁿ \ DR^D where n is the arity of DR
DatatypeRestriction(DR f v)	the n-ary relation over Δ_D obtained by applying the facet f with value v to the data range DR as specified in [XML Schema Datatypes]

We extend the class interpretation function .^Ic to descriptions as shown in Table 3. With #S we denote the number of elements in a set S.

Table 3. Interpreting Descriptions
Description	Interpretation
owl:Thing	Δ_I
owl:Nothing	empty set
ObjectComplementOf(C)	Δ_I \ C^Ic
ObjectIntersectionOf(C₁ ... C_n)	C₁^Ic ∩ ... ∩ C_n^Ic
ObjectUnionOf(C₁ ... C_n)	C₁^Ic ∪ ... ∪ C_n^Ic
ObjectOneOf(a₁ ... a_n)	{ a₁^Ii , ... , a_n^Ii }
ObjectSomeValuesFrom(R C)	{ x \| ∃ y : ( x, y ) ∈ R^Ipo and y ∈ C^Ic }
ObjectAllValuesFrom(R C)	{ x \| ∀ y : ( x, y ) ∈ R^Ipo implies y ∈ C^Ic }
ObjectHasValue(R a)	{ x \| ( x, a^Ii ) ∈ R^Ipo }
ObjectExistsSelf(R)	{ x \| ( x, x ) ∈ R^Ipo }
ObjectMinCardinality(n R C)	{ x \| #{ y \| ( x, y ) ∈ R^Ipo and y ∈ C^Ic } ≥ n }
ObjectMaxCardinality(n R C)	{ x \| #{ y \| ( x, y ) ∈ R^Ipo and y ∈ C^Ic } ≤ n }
ObjectExactCardinality(n R C)	{ x \| #{ y \| ( x, y ) ∈ R^Ipo and y ∈ C^Ic } = n }
DataSomeValuesFrom(U₁ ... U_n DR)	{ x \| ∃ y₁, ..., y_n : ( x, y_k ) ∈ U_k^Ipd for each 1 ≤ k ≤ n and ( y₁, ..., y_n ) ∈ DR^D }
DataAllValuesFrom(U₁ ... U_n DR)	{ x \| ∀ y₁, ..., y_n : ( x, y_k ) ∈ U_k^Ipd for each 1 ≤ k ≤ n implies ( y₁, ..., y_n ) ∈ DR^D }
DataHasValue(U v)	{ x \| ( x, v^D ) ∈ U^Ipd }
DataMinCardinality(n U DR)	{ x \| #{ y \| ( x, y ) ∈ U^Ipd and y ∈ DR^D } ≥ n }
DataMaxCardinality(n U DR)	{ x \| #{ y \| ( x, y ) ∈ U^Ipd and y ∈ DR^D } ≤ n }
DataExactCardinality(n U DR)	{ x \| #{ y \| ( x, y ) ∈ U^Ipd and y ∈ DR^D } = n }

Satisfaction of OWL 2 axioms in an interpretation I is defined as shown in Table 4. With o we denote the composition of binary relations.

Table 4. Satisfaction of Axioms in an Interpretation
Axiom	Condition
SubClassOf(C D)	C^Ic ⊆ D^Ic
EquivalentClasses(C₁ ... C_n)	C_j^Ic = C_k^Ic for each 1 ≤ j , k ≤ n
DisjointClasses(C₁ ... C_n)	C_j^Ic ∩ C_k^Ic is empty for each 1 ≤ j , k ≤ n and j ≠ k
DisjointUnion(A C₁ ... C_n)	A^Ic = C₁^Ic ∪ ... ∪ C_n^Ic and C_j^Ic ∩ C_k^Ic is empty for each 1 ≤ j , k ≤ n and j ≠ k
SubObjectPropertyOf(R S)	R^Ipo ⊆ S^Ipo
SubObjectPropertyOf(SubObjectPropertyChain(R₁ ... R_n) S)	R₁^Ipo o ... o R_n^Ipo ⊆ S^Ipo
EquivalentObjectProperties(R₁ ... R_n)	R_j^Ipo = R_k^Ipo for each 1 ≤ j , k ≤ n
DisjointObjectProperties(R₁ ... R_n)	R_j^Ipo ∩ R_k^Ipo is empty for each 1 ≤ j , k ≤ n and j ≠ k
ObjectPropertyDomain(R C)	{ x \| ∃ y : (x , y ) ∈ R^Ipo } ⊆ C^Ic
ObjectPropertyRange(R C)	{ y \| ∃ x : (x , y ) ∈ R^Ipo } ⊆ C^Ic
InverseObjectProperties(R S)	R^Ipo = { ( x , y ) \| ( y , x ) ∈ S^Ipo }
FunctionalObjectProperty(R)	( x , y₁ ) ∈ R^Ipo and ( x , y₂ ) ∈ R^Ipo imply y₁ = y₂
InverseFunctionalObjectProperty(R)	( x₁ , y ) ∈ R^Ipo and ( x₂ , y ) ∈ R^Ipo imply x₁ = x₂
ReflexiveObjectProperty(R)	x ∈ Δ_I implies ( x , x ) ∈ R^Ipo
IrreflexiveObjectProperty(R)	x ∈ Δ_I implies ( x , x ) is not in R^Ipo
SymmetricObjectProperty(R)	( x , y ) ∈ R^Ipo implies ( y , x ) ∈ R^Ipo
AsymmetricObjectProperty(R)	( x , y ) ∈ R^Ipo implies ( y , x ) is not in R^Ipo
TransitiveObjectProperty(R)	R^Ipo o R^Ipo ⊆ R^Ipo
SubDataPropertyOf(U V)	U^Ipd ⊆ V^Ipd
EquivalentDataProperties(U₁ ... U_n)	U_j^Ipd = U_k^Ipd for each 1 ≤ j , k ≤ n
DisjointDataProperties(U₁ ... U_n)	U_j^Ipd ∩ U_k^Ipd is empty for each 1 ≤ j , k ≤ n and j ≠ k
DataPropertyDomain(U C)	{ x \| ∃ y : (x , y ) ∈ U^Ipd } ⊆ C^Ic
DataPropertyRange(U DR)	{ y \| ∃ x : (x , y ) ∈ U^Ipd } ⊆ DR^D
FunctionalDataProperty(U)	( x , y₁ ) ∈ U^Ipd and ( x , y₂ ) ∈ U^Ipd imply y₁ = y₂
SameIndividual(a₁ ... a_n)	a_j^Ii = a_k^Ii for each 1 ≤ j , k ≤ n
DifferentIndividuals(a₁ ... a_n)	a_j^Ii ≠ a_k^Ii for each 1 ≤ j , k ≤ n and j ≠ k
ClassAssertion(a C)	a^Ii ∈ C^Ic
ObjectPropertyAssertion(R a b)	( a^Ii , b^Ii ) ∈ R^Ipo
NegativeObjectPropertyAssertion(R a b)	( a^Ii , b^Ii ) is not in R^Ipo
DataPropertyAssertion(U a v)	( a^Ii , v^D ) ∈ U^Ipd
NegativeDataPropertyAssertion(U a v)	( a^Ii , v^D ) is not in U^Ipd

Let O be an OWL 2 ontology with vocabulary V. O is consistent if an interpretation I exists that satisfies all the axioms of the axiom closure of O (the axiom closure of O is defined in [OWL 2 Specification]); such I is then called a model of O. A description C is satisfiable w.r.t. O if there is a model I of O such that C^Ic is not empty. O entails an OWL 2 ontology O' with vocabulary V if every model of O is also a model of O'; furthermore, O and O' are equivalent if O entails O' and O' entails O.

3 References

[Description Logics]

OWL 2 Web Ontology Language:Model-Theoretic Semantics