OWL 2 Web Ontology Language Direct Semantics (original) (raw)
W3C Recommendation 27 October 2009
This version:
http://www.w3.org/TR/2009/REC-owl2-direct-semantics-20091027/
Latest version (series 2):
http://www.w3.org/TR/owl2-direct-semantics/
Latest Recommendation:
http://www.w3.org/TR/owl-direct-semantics
Previous version:
http://www.w3.org/TR/2009/PR-owl2-direct-semantics-20090922/ (color-coded diff)
Editors:
Boris Motik, Oxford University Computing Laboratory
Peter F. Patel-Schneider, Bell Labs Research, Alcatel-Lucent
Bernardo Cuenca Grau, Oxford University Computing Laboratory
Contributors: (in alphabetical order)
Ian Horrocks, Oxford University Computing Laboratory
Bijan Parsia, University of Manchester
Uli Sattler, University of Manchester
Please refer to the errata for this document, which may include some normative corrections.
This document is also available in these non-normative formats: PDF version.
See also translations.
Copyright © 2009 W3C® (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
Abstract
The OWL 2 Web Ontology Language, informally OWL 2, is an ontology language for the Semantic Web with formally defined meaning. OWL 2 ontologies provide classes, properties, individuals, and data values and are stored as Semantic Web documents. OWL 2 ontologies can be used along with information written in RDF, and OWL 2 ontologies themselves are primarily exchanged as RDF documents. The OWL 2 Document Overview describes the overall state of OWL 2, and should be read before other OWL 2 documents.
This document provides the direct model-theoretic semantics for OWL 2, which is compatible with the description logic SROIQ. Furthermore, this document defines the most common inference problems 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/.
XML Schema Datatypes Dependency
OWL 2 is defined to use datatypes defined in the XML Schema Definition Language (XSD). As of this writing, the latest W3C Recommendation for XSD is version 1.0, with version 1.1 progressing toward Recommendation. OWL 2 has been designed to take advantage of the new datatypes and clearer explanations available in XSD 1.1, but for now those advantages are being partially put on hold. Specifically, until XSD 1.1 becomes a W3C Recommendation, the elements of OWL 2 which are based on it should be considered optional, as detailed in Conformance, section 2.3. Upon the publication of XSD 1.1 as a W3C Recommendation, those elements cease to be optional and are to be considered required as otherwise specified.
We suggest that for now developers and users follow the XSD 1.1 Candidate Recommendation. Based on discussions between the Schema and OWL Working Groups, we do not expect any implementation changes will be necessary as XSD 1.1 advances to Recommendation.
Document Unchanged
There have been no changes to the body of this document since the previous version. For details on earlier changes, see the change log.
Please Send Comments
Please send any comments to public-owl-comments@w3.org (public archive). Although work on this document by the OWL Working Group is complete, comments may be addressed in the errata or in future revisions. Open discussion among developers is welcome at public-owl-dev@w3.org (public archive).
Endorsed By W3C
This document has been reviewed by W3C Members, by software developers, and by other W3C groups and interested parties, and is endorsed by the Director as a W3C Recommendation. It is a stable document and may be used as reference material or cited from another document. W3C's role in making the Recommendation is to draw attention to the specification and to promote its widespread deployment. This enhances the functionality and interoperability of the Web.
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.
Table of Contents
- 1 Introduction
- 2 Direct Model-Theoretic Semantics for OWL 2
- 2.1 Vocabulary
- 2.2 Interpretations
* 2.2.1 Object Property Expressions
* 2.2.2 Data Ranges
* 2.2.3 Class Expressions - 2.3 Satisfaction in an Interpretation
* 2.3.1 Class Expression Axioms
* 2.3.2 Object Property Expression Axioms
* 2.3.3 Data Property Expression Axioms
* 2.3.4 Datatype Definitions
* 2.3.5 Keys
* 2.3.6 Assertions
* 2.3.7 Ontologies - 2.4 Models
- 2.5 Inference Problems
- 3 Independence of the Direct Semantics from the Datatype Map in OWL 2 DL (Informative)
- 4 Appendix: Change Log (Informative)
- 5 Acknowledgments
- 6 References
1 Introduction
This document defines the direct model-theoretic semantics of OWL 2. The semantics given here is strongly related to the semantics of description logics [Description Logics] and it extends 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 structural specification of OWL 2 [OWL 2 Specification] instead of by reference to SROIQ. For the constructs available in SROIQ, the semantics of SROIQ trivially corresponds to the one defined in this document.
Since each OWL 1 DL ontology is an OWL 2 ontology, this document also provides a direct semantics for OWL 1 Lite and OWL 1 DL ontologies; this semantics is equivalent to the direct model-theoretic semantics of OWL 1 Lite and OWL 1 DL [OWL 1 Semantics and Abstract Syntax]. Furthermore, this document also provides the direct model-theoretic semantics for the OWL 2 profiles [OWL 2 Profiles].
The semantics is defined for OWL 2 axioms and ontologies, which should be understood as instances of the structural specification [OWL 2 Specification]. Parts of the structural specification are written in this document using the functional-style syntax.
OWL 2 allows ontologies, anonymous individuals, and axioms to be annotated; furthermore, annotations themselves can contain additional annotations. All these types of annotations, however, have no semantic meaning in OWL 2 and are ignored in this document. OWL 2 declarations are used only 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 this document.
2 Direct Model-Theoretic Semantics for OWL 2
This section specifies the direct model-theoretic semantics of OWL 2 ontologies.
2.1 Vocabulary
A datatype map, formalizing datatype maps from the OWL 2 Specification [OWL 2 Specification], is a 6-tuple D = ( NDT , NLS , NFS , ⋅ DT , ⋅ LS , ⋅ FS ) with the following components:
- NDT is a set of datatypes (more precisely, names of datatypes) that does not contain the datatype rdfs:Literal.
- NLS is a function that assigns to each datatype DT ∈ NDT a set NLS(DT) of strings called lexical forms. The set NLS(DT) is called the lexical space of DT.
- NFS is a function that assigns to each datatype DT ∈ NDT a set NFS(DT) of pairs ( F , v ), where F is a constraining facet and v is an arbitrary data value called the constraining value. The set NFS(DT) is called the facet space of DT.
- For each datatype DT ∈ NDT, the interpretation function ⋅ DT assigns to DT a set (DT)DT called the value space of DT.
- For each datatype DT ∈ NDT and each lexical form LV ∈ NLS(DT), the interpretation function ⋅ LS assigns to the pair ( LV , DT ) a data value ( LV , DT )LS ∈ (DT)DT.
- For each datatype DT ∈ NDT and each pair ( F , v ) ∈ NFS(DT), the interpretation function ⋅ FS assigns to ( F , v ) the set ( F , v )FS ⊆ (DT)DT.
The set of datatypes NDT of a datatype map D is not required to contain all datatypes from the OWL 2 datatype map; this allows one to talk about subsets of the OWL 2 datatype map, which may be necessary for the various profiles of OWL 2. If, however, D contains a datatype DT from the OWL 2 datatype map, then NLS(DT), NFS(DT), (DT)DT, ( LV , DT )LS for each LV ∈ NLS(DT), and ( F , v )FS for each ( F , v ) ∈ NFS(DT) are required to coincide with the definitions for DT in the OWL 2 datatype map.
A vocabulary V = ( VC , VOP , VDP , VI , VDT , VLT , VFA ) over a datatype map D is a 7-tuple consisting of the following elements:
- VC is a set of classes as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the classes owl:Thing and owl:Nothing.
- VOP is a set of object properties as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the object properties owl:topObjectProperty and owl:bottomObjectProperty.
- VDP is a set of data properties as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the data properties owl:topDataProperty and owl:bottomDataProperty.
- VI is a set of individuals (named and anonymous) as defined in the OWL 2 Specification [OWL 2 Specification].
- VDT is a set containing all datatypes of D, the datatype rdfs:Literal, and possibly other datatypes; that is, NDT ∪ { rdfs:Literal } ⊆ VDT.
- VLT is a set of literals LV_^^_DT for each datatype DT ∈ NDT and each lexical form LV ∈ NLS(DT).
- VFA is the set of pairs ( F , lt ) for each constraining facet F, datatype DT ∈ NDT, and literal lt ∈ VLT such that ( F , ( LV , DT1 )LS ) ∈ NFS(DT), where LV is the lexical form of lt and DT1 is the datatype of lt.
Given a vocabulary V, the following conventions are used in this document to denote different syntactic parts of OWL 2 ontologies:
- OP denotes an object property;
- OPE denotes an object property expression;
- DP denotes a data property;
- DPE denotes a data property expression;
- C denotes a class;
- CE denotes a class expression;
- DT denotes a datatype;
- DR denotes a data range;
- a denotes an individual (named or anonymous);
- lt denotes a literal; and
- F denotes a constraining facet.
2.2 Interpretations
Given a datatype map D and a vocabulary V over D, an interpretation I = ( ΔI , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) for D and V is a 9-tuple with the following structure:
- ΔI is a nonempty set called the object domain.
- ΔD is a nonempty set disjoint with ΔI called the data domain such that (DT)DT ⊆ ΔD for each datatype DT ∈ VDT.
- ⋅ C is the class interpretation function that assigns to each class C ∈ VC a subset (C)C ⊆ ΔI such that
- (owl:Thing)C = ΔI and
- (owl:Nothing)C = ∅.
- ⋅ OP is the object property interpretation function that assigns to each object property OP ∈ VOP a subset (OP)OP ⊆ ΔI × ΔI such that
- (owl:topObjectProperty)OP = ΔI × ΔI and
- (owl:bottomObjectProperty)OP = ∅.
- ⋅ DP is the data property interpretation function that assigns to each data property DP ∈ VDP a subset (DP)DP ⊆ ΔI × ΔD such that
- (owl:topDataProperty)DP = ΔI × ΔD and
- (owl:bottomDataProperty)DP = ∅.
- ⋅ I is the individual interpretation function that assigns to each individual a ∈ VI an element (a)I ∈ ΔI.
- ⋅ DT is the datatype interpretation function that assigns to each datatype DT ∈ VDT a subset (DT)DT ⊆ ΔD such that
- ⋅ DT is the same as in D for each datatype DT ∈ NDT, and
- (rdfs:Literal)DT = ΔD.
- ⋅ LT is the literal interpretation function that is defined as (lt)LT = ( LV , DT )LS for each lt ∈ VLT, where LV is the lexical form of lt and DT is the datatype of lt.
- ⋅ FA is the facet interpretation function that is defined as ( F , lt )FA = ( F , (lt)LT )FS for each ( F , lt ) ∈ VFA.
The following sections define the extensions of ⋅ OP, ⋅ DT, and ⋅ C to object property expressions, data ranges, and class expressions.
2.2.1 Object Property Expressions
The object property interpretation function ⋅ OP is extended to object property expressions as shown in Table 1.
Table 1. Interpreting Object Property Expressions
Object Property Expression | Interpretation ⋅ OP |
---|---|
ObjectInverseOf( OP ) | { ( x , y ) | ( y , x ) ∈ (OP)OP } |
2.2.2 Data Ranges
The datatype interpretation function ⋅ DT is extended to data ranges as shown in Table 3. All datatypes in OWL 2 are unary, so each datatype DT is interpreted as a unary relation over ΔD — that is, as a set (DT)DT ⊆ ΔD. OWL 2 currently does not define data ranges of arity more than one; however, by allowing for _n_-ary data ranges, the syntax of OWL 2 provides a "hook" allowing implementations to introduce extensions such as comparisons and arithmetic. An _n_-ary data range DR is interpreted as an _n_-ary relation (DR)DT over ΔD — that is, as a set (DT)DT ⊆ (ΔD)n
Table 3. Interpreting Data Ranges
Data Range | Interpretation ⋅ DT |
---|---|
DataIntersectionOf( DR1 ... DRn ) | (DR1)DT ∩ ... ∩ (DRn)DT |
DataUnionOf( DR1 ... DRn ) | (DR1)DT ∪ ... ∪ (DRn)DT |
DataComplementOf( DR ) | (ΔD)n \ (DR)DT where n is the arity of DR |
DataOneOf( lt1 ... ltn ) | { (lt1)LT , ... , (ltn)LT } |
DatatypeRestriction( DT F1 lt1 ... Fn ltn ) | (DT)DT ∩ ( F1 , lt1 )FA ∩ ... ∩ ( Fn , ltn )FA |
2.2.3 Class Expressions
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.
Table 4. Interpreting Class Expressions
Class Expression | Interpretation ⋅ C | |
---|---|---|
ObjectIntersectionOf( CE1 ... CEn ) | (CE1)C ∩ ... ∩ (CEn)C | |
ObjectUnionOf( CE1 ... CEn ) | (CE1)C ∪ ... ∪ (CEn)C | |
ObjectComplementOf( CE ) | ΔI \ (CE)C | |
ObjectOneOf( a1 ... an ) | { (a1)I , ... , (an)I } | |
ObjectSomeValuesFrom( OPE CE ) | { x | ∃ y : ( x, y ) ∈ (OPE)OP and y ∈ (CE)C } | |
ObjectAllValuesFrom( OPE CE ) | { x | ∀ y : ( x, y ) ∈ (OPE)OP implies y ∈ (CE)C } | |
ObjectHasValue( OPE a ) | { x | ( x , (a)I ) ∈ (OPE)OP } | |
ObjectHasSelf( OPE ) | { x | ( x , x ) ∈ (OPE)OP } | |
ObjectMinCardinality( n OPE ) | { x | #{ y | ( x , y ) ∈ (OPE)OP } ≥ n } |
ObjectMaxCardinality( n OPE ) | { x | #{ y | ( x , y ) ∈ (OPE)OP } ≤ n } |
ObjectExactCardinality( n OPE ) | { x | #{ y | ( x , y ) ∈ (OPE)OP } = n } |
ObjectMinCardinality( n OPE CE ) | { x | #{ y | ( x , y ) ∈ (OPE)OP and y ∈ (CE)C } ≥ n } |
ObjectMaxCardinality( n OPE CE ) | { x | #{ y | ( x , y ) ∈ (OPE)OP and y ∈ (CE)C } ≤ n } |
ObjectExactCardinality( n OPE CE ) | { x | #{ y | ( x , y ) ∈ (OPE)OP and y ∈ (CE)C } = n } |
DataSomeValuesFrom( DPE1 ... DPEn DR ) | { x | ∃ y1, ... , yn : ( x , yk ) ∈ (DPEk)DP for each 1 ≤ k ≤ n and ( y1 , ... , yn ) ∈ (DR)DT } | |
DataAllValuesFrom( DPE1 ... DPEn DR ) | { x | ∀ y1, ... , yn : ( x , yk ) ∈ (DPEk)DP for each 1 ≤ k ≤ n imply ( y1 , ... , yn ) ∈ (DR)DT } | |
DataHasValue( DPE lt ) | { x | ( x , (lt)LT ) ∈ (DPE)DP } | |
DataMinCardinality( n DPE ) | { x | #{ y | ( x , y ) ∈ (DPE)DP} ≥ n } |
DataMaxCardinality( n DPE ) | { x | #{ y | ( x , y ) ∈ (DPE)DP } ≤ n } |
DataExactCardinality( n DPE ) | { x | #{ y | ( x , y ) ∈ (DPE)DP } = n } |
DataMinCardinality( n DPE DR ) | { x | #{ y | ( x , y ) ∈ (DPE)DP and y ∈ (DR)DT } ≥ n } |
DataMaxCardinality( n DPE DR ) | { x | #{ y | ( x , y ) ∈ (DPE)DP and y ∈ (DR)DT } ≤ n } |
DataExactCardinality( n DPE DR ) | { x | #{ y | ( x , y ) ∈ (DPE)DP and y ∈ (DR)DT } = n } |
2.3 Satisfaction in an Interpretation
An interpretation I = ( ΔI , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) satisfies an axiom w.r.t. an ontology O if the axiom satisfies the relevant condition from the following sections. Satisfaction of axioms in I is defined w.r.t. O because satisfaction of key axioms uses the following function:
ISNAMEDO(x) = true for x ∈ ΔI if and only if (a)I = x for some named individual a occurring in the axiom closure of O
2.3.1 Class Expression Axioms
Satisfaction of OWL 2 class expression axioms in I w.r.t. O is defined as shown in Table 5.
Table 5. Satisfaction of Class Expression Axioms in an Interpretation
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 |
2.3.2 Object Property Expression Axioms
Satisfaction of OWL 2 object property expression axioms in I w.r.t. O is defined as shown in Table 6.
Table 6. Satisfaction of Object Property Expression Axioms in an Interpretation
Axiom | Condition |
---|---|
SubObjectPropertyOf( OPE1 OPE2 ) | (OPE1)OP ⊆ (OPE2)OP |
SubObjectPropertyOf( ObjectPropertyChain( OPE1 ... OPEn ) OPE ) | ∀ y0 , ... , yn : ( y0 , y1 ) ∈ (OPE1)OP and ... and ( yn-1 , yn ) ∈ (OPEn)OP imply ( y0 , yn ) ∈ (OPE)OP |
EquivalentObjectProperties( OPE1 ... OPEn ) | (OPEj)OP = (OPEk)OP for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointObjectProperties( OPE1 ... OPEn ) | (OPEj)OP ∩ (OPEk)OP = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
ObjectPropertyDomain( OPE CE ) | ∀ x , y : ( x , y ) ∈ (OPE)OP implies x ∈ (CE)C |
ObjectPropertyRange( OPE CE ) | ∀ x , y : ( x , y ) ∈ (OPE)OP implies y ∈ (CE)C |
InverseObjectProperties( OPE1 OPE2 ) | (OPE1)OP = { ( x , y ) | ( y , x ) ∈ (OPE2)OP } |
FunctionalObjectProperty( OPE ) | ∀ x , y1 , y2 : ( x , y1 ) ∈ (OPE)OP and ( x , y2 ) ∈ (OPE)OP imply y1 = y2 |
InverseFunctionalObjectProperty( OPE ) | ∀ x1 , x2 , y : ( x1 , y ) ∈ (OPE)OP and ( x2 , y ) ∈ (OPE)OP imply x1 = x2 |
ReflexiveObjectProperty( OPE ) | ∀ x : x ∈ ΔI implies ( x , x ) ∈ (OPE)OP |
IrreflexiveObjectProperty( OPE ) | ∀ x : x ∈ ΔI implies ( x , x ) ∉ (OPE)OP |
SymmetricObjectProperty( OPE ) | ∀ x , y : ( x , y ) ∈ (OPE)OP implies ( y , x ) ∈ (OPE)OP |
AsymmetricObjectProperty( OPE ) | ∀ x , y : ( x , y ) ∈ (OPE)OP implies ( y , x ) ∉ (OPE)OP |
TransitiveObjectProperty( OPE ) | ∀ x , y , z : ( x , y ) ∈ (OPE)OP and ( y , z ) ∈ (OPE)OP imply ( x , z ) ∈ (OPE)OP |
2.3.3 Data Property Expression Axioms
Satisfaction of OWL 2 data property expression axioms in I w.r.t. O is defined as shown in Table 7.
Table 7. Satisfaction of Data Property Expression Axioms in an Interpretation
Axiom | Condition |
---|---|
SubDataPropertyOf( DPE1 DPE2 ) | (DPE1)DP ⊆ (DPE2)DP |
EquivalentDataProperties( DPE1 ... DPEn ) | (DPEj)DP = (DPEk)DP for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointDataProperties( DPE1 ... DPEn ) | (DPEj)DP ∩ (DPEk)DP = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
DataPropertyDomain( DPE CE ) | ∀ x , y : ( x , y ) ∈ (DPE)DP implies x ∈ (CE)C |
DataPropertyRange( DPE DR ) | ∀ x , y : ( x , y ) ∈ (DPE)DP implies y ∈ (DR)DT |
FunctionalDataProperty( DPE ) | ∀ x , y1 , y2 : ( x , y1 ) ∈ (DPE)DP and ( x , y2 ) ∈ (DPE)DP imply y1 = y2 |
2.3.4 Datatype Definitions
Satisfaction of datatype definitions in I w.r.t. O is defined as shown in Table 8.
Table 8. Satisfaction of Datatype Definitions in an Interpretation
Axiom | Condition |
---|---|
DatatypeDefinition( DT DR ) | (DT)DT = (DR)DT |
2.3.5 Keys
Satisfaction of keys in I w.r.t. O is defined as shown in Table 9.
Table 9. Satisfaction of Keys in an Interpretation
Axiom | Condition |
---|---|
HasKey( CE ( OPE1 ... OPEm ) ( DPE1 ... DPEn ) ) | ∀ x , y , z1 , ... , zm , w1 , ... , wn : if x ∈ (CE)C and ISNAMEDO(x) and y ∈ (CE)C and ISNAMEDO(y) and ( x , zi ) ∈ (OPEi)OP and ( y , zi ) ∈ (OPEi)OP and ISNAMEDO(zi) for each 1 ≤ i ≤ m and ( x , wj ) ∈ (DPEj)DP and ( y , wj ) ∈ (DPEj)DP for each 1 ≤ j ≤ n then x = y |
2.3.6 Assertions
Satisfaction of OWL 2 assertions in I w.r.t. O is defined as shown in Table 10.
Table 10. Satisfaction of Assertions in an Interpretation
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 |
ObjectPropertyAssertion( OPE a1 a2 ) | ( (a1)I , (a2)I ) ∈ (OPE)OP |
NegativeObjectPropertyAssertion( OPE a1 a2 ) | ( (a1)I , (a2)I ) ∉ (OPE)OP |
DataPropertyAssertion( DPE a lt ) | ( (a)I , (lt)LT ) ∈ (DPE)DP |
NegativeDataPropertyAssertion( DPE a lt ) | ( (a)I , (lt)LT ) ∉ (DPE)DP |
2.3.7 Ontologies
An interpretation I satisfies an OWL 2 ontology O if all axioms in the axiom closure of O (with anonymous individuals standardized apart as described in Section 5.6.2 of the OWL 2 Specification [OWL 2 Specification]) are satisfied in I w.r.t. O.
2.4 Models
Given a datatype map D, an interpretation I = ( ΔI , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ I , ⋅ DT , ⋅ LT , ⋅ FA ) for D is a model of an OWL 2 ontology O w.r.t. D if an interpretation J = ( ΔI , ΔD , ⋅ C , ⋅ OP , ⋅ DP , ⋅ J , ⋅ DT , ⋅ LT , ⋅ FA ) for D exists such that ⋅ J coincides with ⋅ I on all named individuals and J satisfies O.
Thus, an interpretation I satisfying O is also a model of O. In contrast, a model I of O may not satisfy O directly; however, by modifying the interpretation of anonymous individuals, I can always be coerced into an interpretation J that satisfies O.
2.5 Inference Problems
Let D be a datatype map and V a vocabulary over D. Furthermore, let O and O1 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. Furthermore, variables are symbols that are not contained in V. Finally, 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 O1 w.r.t. D if every model of O w.r.t. D and V is also a model of O1 w.r.t. D and V.
Ontology Equivalence: O and O1 are equivalent w.r.t. D if O entails O1 w.r.t. D and O1 entails O w.r.t. D.
Ontology Equisatisfiability: O and O1 are equisatisfiable w.r.t. D if O is satisfiable w.r.t. D if and only if O1 is satisfiable w.r.t D.
Class Expression Satisfiability: CE is satisfiable w.r.t. O and D if a model I = ( ΔI , Δ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 I = ( ΔI , Δ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 I = ( ΔI , Δ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 according to the standard definitions of first-order logic.
In order to ensure that ontology entailment, class expression satisfiability, class expression subsumption, and instance checking are decidable, the following restriction w.r.t. O needs to be satisfied:
Each class expression of type MinObjectCardinality, MaxObjectCardinality, ExactObjectCardinality, and ObjectHasSelf that occurs in O1, CE, CE1, and CE2 can contain only object property expressions that are simple in the axiom closure Ax of O.
For ontology equivalence to be decidable, O1 needs to satisfy this restriction w.r.t. O and vice versa. These restrictions are analogous to the first condition from Section 11.2 of the OWL 2 Specification [OWL 2 Specification].
3 Independence of the Direct Semantics from the Datatype Map in OWL 2 DL (Informative)
OWL 2 DL has been defined so that the consequences of an OWL 2 DL ontology O do 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, and it has several useful consequences:
- One can apply the direct semantics to an OWL 2 DL ontology O by considering only the datatypes explicitly occurring in O.
- When referring to various reasoning problems, the datatype map D need not be given explicitly, as it is sufficient to consider an implicit datatype map containing only the datatypes from the given ontology.
- OWL 2 DL reasoners can provide datatypes not explicitly mentioned in this specification without fear that this will change the meaning of OWL 2 DL ontologies not using these datatypes.
Theorem DS1. Let O1 and O2 be OWL 2 DL ontologies over a vocabulary V and D = ( NDT , NLS , NFS , ⋅ DT , ⋅ LS , ⋅ FS ) a datatype map such that each datatype mentioned in O1 and O2 is rdfs:Literal, a datatype defined in the respective ontology, or it occurs in NDT. Furthermore, let D' = ( NDT' , NLS' , NFS' , ⋅ DT ' , ⋅ LS ' , ⋅ FS ' ) be a datatype map such that NDT ⊆ NDT', NLS(DT) = NLS'(DT), and NFS(DT) = NFS'(DT) for each DT ∈ NDT, and ⋅ DT ', ⋅ LS ', and ⋅ FS ' are extensions of ⋅ DT, ⋅ LS, and ⋅ FS, 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]. Furthermore, since datatype definitions in O1 and O2 are acyclic, one can assume that each defined datatype has been recursively replaced with its definition; thus, all datatypes in O1 and O2 are from NDT ∪ { rdfs:Literal }. The claim of the theorem is equivalent to the following statement: an interpretation I w.r.t. D and V exists such that O1 is and O2 is not satisfied in I if and only if an interpretation I' w.r.t. D' and V exists such that O1 is and O2 is not satisfied in I'. The (⇐) direction is trivial since each interpretation I w.r.t. D' and V is also an interpretation w.r.t. D and V. For the (⇒) direction, assume that an interpretation I = ( ΔI , Δ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 I. Let I' = ( ΔI , ΔD' , ⋅ C ' , ⋅ OP , ⋅ DP ' , ⋅ I , ⋅ DT ' , ⋅ LT ' , ⋅ FA ' ) be an interpretation such that
- ΔD' is obtained by extending ΔD with the value space of all datatypes in NDT' \ NDT,
- ⋅ C ' coincides with ⋅ C on all classes, and
- ⋅ DP ' coincides with ⋅ DP on all data properties apart from owl:topDataProperty.
Clearly, DataComplementOf( DR )DT ⊆ DataComplementOf( DR )DT ' for each data range DR that is either a datatype, a datatype restriction, or an enumerated data range. The owl:topDataProperty property can occur in O1 and O2 only in tautologies. The interpretation of all other data properties is the same in I and I', so (CE)C = (CE)C ' for each class expression CE occurring in O1 and O2. Therefore, O1 is and O2 is not satisfied in I'. QED
5 Acknowledgments
The starting point for the development of OWL 2 was the OWL1.1 member submission, itself a result of user and developer feedback, and in particular of information gathered during the OWL Experiences and Directions (OWLED) Workshop series. The working group also considered postponed issues from the WebOnt Working Group.
This document has been produced by the OWL Working Group (see below), and its contents reflect extensive discussions within the Working Group as a whole. The editors extend special thanks to Markus Krötzsch (FZI), Michael Schneider (FZI) and Thomas Schneider (University of Manchester) for their thorough reviews.
The regular attendees at meetings of the OWL Working Group at the time of publication of this document were: Jie Bao (RPI), Diego Calvanese (Free University of Bozen-Bolzano), Bernardo Cuenca Grau (Oxford University Computing Laboratory), Martin Dzbor (Open University), Achille Fokoue (IBM Corporation), Christine Golbreich (Université de Versailles St-Quentin and LIRMM), Sandro Hawke (W3C/MIT), Ivan Herman (W3C/ERCIM), Rinke Hoekstra (University of Amsterdam), Ian Horrocks (Oxford University Computing Laboratory), Elisa Kendall (Sandpiper Software), Markus Krötzsch (FZI), Carsten Lutz (Universität Bremen), Deborah L. McGuinness (RPI), Boris Motik (Oxford University Computing Laboratory), Jeff Pan (University of Aberdeen), Bijan Parsia (University of Manchester), Peter F. Patel-Schneider (Bell Labs Research, Alcatel-Lucent), Sebastian Rudolph (FZI), Alan Ruttenberg (Science Commons), Uli Sattler (University of Manchester), Michael Schneider (FZI), Mike Smith (Clark & Parsia), Evan Wallace (NIST), Zhe Wu (Oracle Corporation), and Antoine Zimmermann (DERI Galway). We would also like to thank past members of the working group: Jeremy Carroll, Jim Hendler, Vipul Kashyap.
6 References
6.1 Normative References
[OWL 2 Specification]
OWL 2 Web Ontology Language: Structural Specification and Functional-Style Syntax Boris Motik, Peter F. Patel-Schneider, Bijan Parsia, eds. W3C Recommendation, 27 October 2009, http://www.w3.org/TR/2009/REC-owl2-syntax-20091027/. Latest version available at http://www.w3.org/TR/owl2-syntax/.
6.2 Nonnormative References
[Description Logics]
The Description Logic Handbook: Theory, Implementation, and Applications, second edition. Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider, eds. Cambridge University Press, 2007. Also see the Description Logics Home Page.
[OWL 1 Semantics and Abstract Syntax]
OWL Web Ontology Language: Semantics and Abstract Syntax. Peter F. Patel-Schneider, Patrick Hayes, and Ian Horrocks, eds. W3C Recommendation, 10 February 2004, http://www.w3.org/TR/2004/REC-owl-semantics-20040210/. Latest version available at http://www.w3.org/TR/owl-semantics/.
[OWL 2 Profiles]
OWL 2 Web Ontology Language: Profiles Boris Motik, Bernardo Cuenca Grau, Ian Horrocks, Zhe Wu, Achille Fokoue, Carsten Lutz, eds. W3C Recommendation, 27 October 2009, http://www.w3.org/TR/2009/REC-owl2-profiles-20091027/. Latest version available at http://www.w3.org/TR/owl2-profiles/.
[SROIQ]
The Even More Irresistible SROIQ. Ian Horrocks, Oliver Kutz, and Uli Sattler. In Proc. of the 10th Int. Conf. on Principles of Knowledge Representation and Reasoning (KR 2006). AAAI Press, 2006.