Copyright © 2008 W3C® (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
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 7 documents:
The OWL Working Group intends to make OWL 2 be a superset of OWL 1, except for a limited number of situations where we believe the impact will be minimal. This means that OWL 2 will be backward compatible, and creators of OWL 1 documents need only move to OWL 2 when they want to make use of OWL 2 features. More details and advice concerning migration from OWL 1 to OWL 2 will be in future drafts.
There are several major changes to this document since the version of 11 April 2008. A number of changes reflect the major revamping of the functional syntax to disallow punning between classes and datatypes and between object, data, and annotation properties. Semantics of Keys has been added. A set of inference problems has been defined. An extended discussion of datatypes has been added. Some minor changes were made to reflect changes in the Functional Syntax.
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.
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.
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.
Contents |
This document defines the formal, model-theoretic semantics of OWL 2. The semantics given here is strongly related to the semantics of description logics [Description Logics] and is compatible with the semantics of the description logic SROIQ [SROIQ]. As the definition of SROIQ does not provide for datatypes and punning, the semantics of OWL 2 is defined directly on the constructs of the functional-style syntax for OWL 2 [OWL 2 Specification] instead of by reference to the semantics of SROIQ. For the constructs available in SROIQ, the semantics of SROIQ trivially corresponds to the one defined 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; this semantics is equivalent to the official semantics of OWL Lite and OWL DL [OWL Abstract Syntax and Semantics]. Furthermore, this document also provides the model-theoretic semantics for the OWL 2 profiles [OWL 2 Profiles].
The semantics is defined for a set of axioms, rather than for an ontology document in the functional-style syntax. Turning ontology documents into sets of axioms involves determining the axiom closure of an ontology (i.e., performing imports and renaming anonymous individuals apart) as described in the OWL 2 Specification [OWL 2 Specification]).
OWL 2 allows for annotations of ontologies, ontology entities (classes, properties, and individuals), anonymous individuals, axioms, and other annotations. Annotations of all these types, however, have no semantic meaning in OWL 2 and are ignored in this document. OWL 2 declarations are simply used to disambiguate class expressions from data ranges and object property from data property expressions in the functional-style syntax. Therefore, they are not mentioned explicitly in the tables in this document.
This section specifies the model-theoretic semantics of OWL 2 ontologies in the functional-style syntax.
Let D = ( NDT , NLT , NFA , ⋅ DT , ⋅ LT , ⋅ FA ) be a datatype map as defined in Section 4 of the OWL 2 Specification [OWL 2 Specification], interpreting the built-in datatypes as defined in Sections 4.1 to 4.6. A vocabulary V = ( VC , VOP , VDP , VI , VDT , VLT , VFA ) over D is a 7-tuple consisting of the following elements:
Given a vocabulary V, the following conventions are used in this document to denote different syntactic parts of OWL 2 ontologies:
Given a datatype map D and a vocabulary V over D, an interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) for D and V is a 9-tuple with the following structure.
The following sections define the extensions of ⋅ OP, ⋅ DT, and ⋅ C to object property expressions, data ranges, and class expressions.
The object property interpretation function ⋅ OP is extended to object property expressions as shown in Table 1.
Object Property Expression | Interpretation ⋅ OP |
---|---|
InverseOf( OP ) | { 〈 x , y 〉 | 〈 y , x 〉 ∈ (OP)OP } |
The datatype interpretation function ⋅ DT is extended to data ranges as shown in Table 3. Note that datatypes in OWL 2 are all unary; thus, each datatype DT is interpreted as a unary relation (DT)DT over ΔD. Data ranges, however, can be n-ary—this allows implementations to provide built-in predicates such as comparisons or arithmetic as an extension. Hence, an n-ary data range DR is interpreted as an n-ary relation (DR)DT over ΔD.
Data Range | Interpretation ⋅ DT |
---|---|
OneOf( lt1 ... ltn ) | { (lt1)LT , ... , (ltn)LT } |
ComplementOf( DR ) | (ΔD)n \ (DR)DT where n is the arity of DR |
DatatypeRestriction( DT f1 lt1 ... fn ltn ) | (DT)DT ∩ (〈 f1 lt1 〉)FA ∩ ... ∩ (〈 fn ltn 〉)FA |
The class interpretation function ⋅ C is extended to class expressions as shown in Table 4. For S a set, #S denotes the number of elements in S.
Class Expression | Interpretation ⋅ C |
---|---|
IntersectionOf( CE1 ... CEn ) | (CE1)C ∩ ... ∩ (CEn)C |
UnionOf( CE1 ... CEn ) | (CE1)C ∪ ... ∪ (CEn)C |
ComplementOf( CE ) | ΔInt \ (CE)C |
OneOf( a1 ... an ) | { (a1)I , ... , (an)I } |
SomeValuesFrom( OPE CE ) | { x | ∃ y : 〈 x, y 〉 ∈ (OPE)OP and y ∈ (CE)C } |
AllValuesFrom( OPE CE ) | { x | ∀ y : 〈 x, y 〉 ∈ (OPE)OP implies y ∈ (CE)C } |
HasValue( OPE a ) | { x | 〈 x , (a)I 〉 ∈ (OPE)OP } |
ExistsSelf( OPE ) | { x | 〈 x , x 〉 ∈ (OPE)OP } |
MinCardinality( n OPE ) | { x | #{ y | 〈 x , y 〉 ∈ (OPE)OP } ≥ n } |
MaxCardinality( n OPE ) | { x | #{ y | 〈 x , y 〉 ∈ (OPE)OP } ≤ n } |
ExactCardinality( n OPE ) | { x | #{ y | 〈 x , y 〉 ∈ (OPE)OP } = n } |
MinCardinality( n OPE CE ) | { x | #{ y | 〈 x , y 〉 ∈ (OPE)OP and y ∈ (CE)C } ≥ n } |
MaxCardinality( n OPE CE ) | { x | #{ y | 〈 x , y 〉 ∈ (OPE)OP and y ∈ (CE)C } ≤ n } |
ExactCardinality( n OPE CE ) | { x | #{ y | 〈 x , y 〉 ∈ (OPE)OP and y ∈ (CE)C } = n } |
SomeValuesFrom( DPE1 ... DPEn DR ) | { x | ∃ y1, ... , yn : 〈 x , yk 〉 ∈ (DPEk)DP for each 1 ≤ k ≤ n and 〈 y1 , ... , yn 〉 ∈ (DR)DT } |
AllValuesFrom( DPE1 ... DPEn DR ) | { x | ∀ y1, ... , yn : 〈 x , yk 〉 ∈ (DPEk)DP for each 1 ≤ k ≤ n imply 〈 y1 , ... , yn 〉 ∈ (DR)DT } |
HasValue( DPE lt ) | { x | 〈 x , (lt)LT 〉 ∈ (DPE)DP } |
MinCardinality( n DPE ) | { x | #{ y | 〈 x , y 〉 ∈ (DPE)DP} ≥ n } |
MaxCardinality( n DPE ) | { x | #{ y | 〈 x , y 〉 ∈ (DPE)DP } ≤ n } |
ExactCardinality( n DPE ) | { x | #{ y | 〈 x , y 〉 ∈ (DPE)DP } = n } |
MinCardinality( n DPE DR ) | { x | #{ y | 〈 x , y 〉 ∈ (DPE)DP and y ∈ (DR)DT } ≥ n } |
MaxCardinality( n DPE DR ) | { x | #{ y | 〈 x , y 〉 ∈ (DPE)DP and y ∈ (DR)DT } ≤ n } |
ExactCardinality( n DPE DR ) | { x | #{ y | 〈 x , y 〉 ∈ (DPE)DP and y ∈ (DR)DT } = n } |
An interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) satisfies an axiom w.r.t. an ontology O if the axiom satisfies appropriate conditions listed in the following sections. Satisfaction of axioms in Int is defined w.r.t. O because satisfaction of key axioms uses the function ISNAMEDO defined as follows, where the axiom closure of O is defined in Section 3.4 of the OWL 2 Specification [OWL 2 Specification]:
ISNAMEDO(x) = true for x ∈ ΔInt if and only if (a)I = x for some named individual a occurring in the axiom closure of O.
Satisfaction of OWL 2 class expression axioms in Int w.r.t. O is defined as shown in Table 5.
Axiom | Condition |
---|---|
SubClassOf( CE1 CE2 ) | (CE1)C ⊆ (CE2)C |
EquivalentClasses( CE1 ... CEn ) | (CEj)C = (CEk)C for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointClasses( CE1 ... CEn ) | (CEj)C ∩ (CEk)C = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
DisjointUnion( C CE1 ... CEn ) | (C)C = (CE1)C ∪
... ∪ (CEn)C and (CEj)C ∩ (CEk)C = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
Satisfaction of OWL 2 object property expression axioms in Int w.r.t. O is defined as shown in Table 6.
Axiom | Condition |
---|---|
SubPropertyOf( OPE1 OPE2 ) | (OPE1)OP ⊆ (OPE2)OP |
SubPropertyOf( PropertyChain( OPE1 ... OPEn ) OPE ) | ∀ y0 , ... , yn : 〈 y0 , y1 〉 ∈ (OPE1)OP and ... and 〈 yn-1 , yn 〉 ∈ (OPEn)OP imply 〈 y0 , yn 〉 ∈ (OPE)OP |
EquivalentProperties( OPE1 ... OPEn ) | (OPEj)OP = (OPEk)OP for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointProperties( OPE1 ... OPEn ) | (OPEj)OP ∩ (OPEk)OP = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
PropertyDomain( OPE CE ) | ∀ x , y : 〈 x , y 〉 ∈ (OPE)OP implies x ∈ (CE)C |
PropertyRange( OPE CE ) | ∀ x , y : 〈 x , y 〉 ∈ (OPE)OP implies y ∈ (CE)C |
InverseProperties( OPE1 OPE2 ) | (OPE1)OP = { 〈 x , y 〉 | 〈 y , x 〉 ∈ (OPE2)OP } |
FunctionalProperty( OPE ) | ∀ x , y1 , y2 : 〈 x , y1 〉 ∈ (OPE)OP and 〈 x , y2 〉 ∈ (OPE)OP imply y1 = y2 |
InverseFunctionalProperty( OPE ) | ∀ x1 , x2 , y : 〈 x1 , y 〉 ∈ (OPE)OP and 〈 x2 , y 〉 ∈ (OPE)OP imply x1 = x2 |
ReflexiveProperty( OPE ) | ∀ x : x ∈ ΔInt implies 〈 x , x 〉 ∈ (OPE)OP |
IrreflexiveProperty( OPE ) | ∀ x : x ∈ ΔInt implies 〈 x , x 〉 ∉ (OPE)OP |
SymmetricProperty( OPE ) | ∀ x , y : 〈 x , y 〉 ∈ (OPE)OP implies 〈 y , x 〉 ∈ (OPE)OP |
AsymmetricProperty( OPE ) | ∀ x , y : 〈 x , y 〉 ∈ (OPE)OP implies 〈 y , x 〉 ∉ (OPE)OP |
TransitiveProperty( OPE ) | ∀ x , y , z : 〈 x , y 〉 ∈ (OPE)OP and 〈 y , z 〉 ∈ (OPE)OP imply 〈 x , z 〉 ∈ (OPE)OP |
Satisfaction of OWL 2 data property expression axioms in Int w.r.t. O is defined as shown in Table 7.
Axiom | Condition |
---|---|
SubPropertyOf( DPE1 DPE2 ) | (DPE1)DP ⊆ (DPE2)DP |
EquivalentProperties( DPE1 ... DPEn ) | (DPEj)DP = (DPEk)DP for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointProperties( DPE1 ... DPEn ) | (DPEj)DP ∩ (DPEk)DP = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
PropertyDomain( DPE CE ) | ∀ x , y : 〈 x , y 〉 ∈ (DPE)DP implies x ∈ (CE)C |
PropertyRange( DPE DR ) | ∀ x , y : 〈 x , y 〉 ∈ (DPE)DP implies y ∈ (DR)DT |
FunctionalProperty( DPE ) | ∀ x , y1 , y2 : 〈 x , y1 〉 ∈ (DPE)DP and 〈 x , y2 〉 ∈ (DPE)DP imply y1 = y2 |
Satisfaction of keys in Int w.r.t. O is defined as shown in Table 8.
Axiom | Condition |
---|---|
HasKey( CE PE1 ... PEn ) | ∀ x , y ,
z1 , ... , zn : if ISNAMEDO(x) and ISNAMEDO(y) and ISNAMEDO(z1) and ... and ISNAMEDO(zn) and x ∈ (CE)C and y ∈ (CE)C and for each 1 ≤ i ≤ n, if PEi is an object property, then 〈 x , zi 〉 ∈ (PEi)OP and 〈 y , zi 〉 ∈ (PEi)OP, and if PEi is a data property, then 〈 x , zi 〉 ∈ (PEi)DP and 〈 y , zi 〉 ∈ (PEi)DP then x = y |
Satisfaction of OWL 2 assertions in Int w.r.t. O is defined as shown in Table 9.
Axiom | Condition |
---|---|
SameIndividual( a1 ... an ) | (aj)I = (ak)I for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DifferentIndividuals( a1 ... an ) | (aj)I ≠ (ak)I for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
ClassAssertion( CE a ) | (a)I ∈ (CE)C |
PropertyAssertion( OPE a1 a2 ) | 〈 (a1)I , (a2)I 〉 ∈ (OPE)OP |
NegativePropertyAssertion( OPE a1 a2 ) | 〈 (a1)I , (a2)I 〉 ∉ (OPE)OP |
PropertyAssertion( DPE a lt ) | 〈 (a)I , (lt)LT 〉 ∈ (DPE)DP |
NegativePropertyAssertion( DPE a lt ) | 〈 (a)I , (lt)LT 〉 ∉ (DPE)DP |
Int satisfies an OWL 2 ontology O if all axioms in the axiom closure of O (with anonymous individuals renamed apart as described in Section 5.6.2 of the OWL 2 Specification [OWL 2 Specification]) are satisfied in Int w.r.t. O.
An interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) is a model of an OWL 2 ontology O if an interpretation Int' = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I' , ⋅ DT , ⋅ LT , ⋅ FA ) exists such that ⋅ I' coincides with ⋅ I on all named individuals and Int' satisfies O.
Thus, an interpretation Int satisfying O is also a model of O. In contrast, a model Int of O may not satisfy O directly; however, by modifying the interpretation of anonymous individuals, Int can always be coerced into an interpretation Int' that satisfies O.
Let D be a datatype map and V a vocabulary over D. Furthermore, let O and O' be OWL 2 ontologies, CE, CE1, and CE2 class expressions, and a a named individual, such that all of them refer only to the vocabulary elements in V. A Boolean conjunctive query Q is a closed formula of the form [ ∃ x1 , ... , xn , y1 , ... , ym : A1 ∧ ... ∧ Ak ], where each Ai is an atom of the form C(s), OP(s,t), or DP(s,u) with C a class, OP an object property, DP a data property, s and t individuals or some variable xj, and u a literal or some variable yj.
The following inference problems are often considered in practice.
Ontology Consistency: O is consistent (or satisfiable') w.r.t. D if a model of O w.r.t. D and V exists.
Ontology Entailment: O entails O' w.r.t. D if every model of O w.r.t. D and V is also a model of O' w.r.t. D and V.
Ontology Equivalence: O and O' are equivalent w.r.t. D if O entails O' w.r.t. D and O' entails O w.r.t. D.
Ontology Equisatisfiability: O and O' are equisatisfiable w.r.t. D if O is satisfiable w.r.t. D if and only if O' is satisfiable w.r.t D.
Class Expression Satisfiability: CE is satisfiable w.r.t. O and D if a model Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) of O w.r.t. D and V exists such that (CE)C ≠ ∅.
Class Expression Subsumption: CE1 is subsumed by a class expression CE2 w.r.t. O and D if (CE1)C ⊆ (CE2)C for each model Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) of O w.r.t. D and V.
Instance Checking: a is an instance of CE w.r.t. O and D if (a)I ∈ (CE)C for each model Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) of O w.r.t. D and V.
Boolean Conjunctive Query Answering: Q is an answer w.r.t. O and D if Q is true in each model of O w.r.t. D and V.
The semantics of OWL 2 has been defined in such a way that the semantics of an OWL 2 ontology O does not depend on the choice of a datatype map, as long as the datatype map chosen contains all the datatypes occurring in O. This statement is made precise by the following theorem, which has several useful consequences:
Theorem 1. Let O1 and O2 be OWL 2 ontologies over a vocabulary V and D = ( NDT , NLT , NFA , ⋅ DT , ⋅ LT , ⋅ FA ) a datatype map such that each datatype mentioned in O1 and O2 is either rdfs:Literal or it occurs in NDT. Furthermore, let D' = ( NDT' , NLT' , NFA' , ⋅ DT ' , ⋅ LT ' , ⋅ FA ' ) be a datatype map such that NDT ⊆ NDT', NLT(DT) = NLT'(DT) and NFA(DT) = NFA'(DT) for each DT ∈ NDT, and ⋅ DT ', ⋅ LT ', and ⋅ FA ' are extensions of ⋅ DT, ⋅ LT, and ⋅ FA, respectively. Then, O1 entails O2 w.r.t. D if and only if O1 entails O2 w.r.t. D'.
Proof. Without loss of generality, one can assume O1 and O2 to be in negation-normal form [Description Logics]. The claim of the theorem is equivalent to the following statement: an interpretation Int w.r.t. D and and V exists such that O1 is and O2 is not satisfied in Int if and only if an interpretation Int' w.r.t. D' and V exists such that O1 is and O2 is not satisfied in Int'. The (⇐) direction is trivial since each interpretation Int w.r.t. D' and V is also an interpretation w.r.t. D and V. For the (⇒) direction, assume that an interpretation Int = ( ΔInt , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) w.r.t. D and V exists such that O1 is and O2 is not satisfied in Int. Let Int' = ( ΔInt , ΔD' , ⋅ C ' , ⋅ OP , ⋅ DP ' , ⋅ I , ⋅ DT ' , ⋅ LT ' , ⋅ FA ' ) be an interpretation such that
Clearly, ComplementOf( DR )DT ⊆ ComplementOf( DR )DT ' for each data range DR that is is either a datatype, a datatype restriction, or an enumerated data range. The interpretation of data properties is the same in Int and Int', so (CE)C = (CE)C ' for each class expression CE occurring in O1 and O2. Therefore, O1 is and O2 is not satisfied in Int'. QED