Difference between revisions of "Direct Semantics"
(link to definition of axiom closure) |
(fix ups for conjunctive query answering) |
||
Line 407: | Line 407: | ||
=== Inference Problems === | === Inference Problems === | ||
+ | |||
+ | In this section variables are a new kind of syntactic construct, disjoint from the syntactic constructs of OWL 2. | ||
Let ''D'' be a datatype map and ''V'' a vocabulary over ''D''. Furthermore, let ''O'' and ''O<sub>1</sub>'' be OWL 2 ontologies, ''CE'', ''CE<sub>1</sub>'', and ''CE<sub>2</sub>'' class expressions, and ''a'' a named individual, such that all of them refer only to the vocabulary elements in ''V''. A <span id="def_boolean_conjunctive_query">''Boolean conjunctive query''</span> ''Q'' is a closed formula of the form | Let ''D'' be a datatype map and ''V'' a vocabulary over ''D''. Furthermore, let ''O'' and ''O<sub>1</sub>'' be OWL 2 ontologies, ''CE'', ''CE<sub>1</sub>'', and ''CE<sub>2</sub>'' class expressions, and ''a'' a named individual, such that all of them refer only to the vocabulary elements in ''V''. A <span id="def_boolean_conjunctive_query">''Boolean conjunctive query''</span> ''Q'' is a closed formula of the form | ||
Line 432: | Line 434: | ||
'''Instance Checking''': ''a'' is an ''instance'' of ''CE'' w.r.t. ''O'' and ''D'' if ''(a)<sup>I</sup>'' ∈ ''(CE)<sup>C</sup>'' for each model ''Int'' = ( ''Δ<sub>Int</sub>'' , ''Δ<sub>D</sub>'' , ''⋅ <sup>C</sup>'' , ''⋅ <sup>OP</sup>'' , ''⋅ <sup>DP</sup>'' , ''⋅ <sup>I</sup>'' , ''⋅ <sup>DT</sup>'' , ''⋅ <sup>LT</sup>'' , ''⋅ <sup>FA</sup>'' ) of ''O'' w.r.t. ''D'' and ''V''. | '''Instance Checking''': ''a'' is an ''instance'' of ''CE'' w.r.t. ''O'' and ''D'' if ''(a)<sup>I</sup>'' ∈ ''(CE)<sup>C</sup>'' for each model ''Int'' = ( ''Δ<sub>Int</sub>'' , ''Δ<sub>D</sub>'' , ''⋅ <sup>C</sup>'' , ''⋅ <sup>OP</sup>'' , ''⋅ <sup>DP</sup>'' , ''⋅ <sup>I</sup>'' , ''⋅ <sup>DT</sup>'' , ''⋅ <sup>LT</sup>'' , ''⋅ <sup>FA</sup>'' ) 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''. | + | '''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'', making the usual changes needed to account for quantification and variables. |
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: | 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: |
Revision as of 19:45, 11 February 2009
__NUMBEREDHEADINGS__
- Document title:
- OWL 2 Web Ontology Language
Direct Semantics (Second Edition)
- Editors
- Boris Motik, Oxford University
- Peter F. Patel-Schneider, Bell Labs Research, Alcatel-Lucent
- Bernardo Cuenca Grau, Oxford University
- Contributors (alphabetical order)
- Ian Horrocks, Oxford University
- Bijan Parsia, University of Manchester
- Uli Sattler, University of Manchester
- 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
Copyright © 2008-2009 W3C^{®} (MIT, ERCIM, Keio), All Rights Reserved. W3C liability, trademark and document use rules apply.
Contents
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 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 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 OWL 2 is an extension of OWL DL, this document also provides a direct 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 direct model-theoretic semantics for the OWL 2 profiles [OWL 2 Profiles].
The semantics is defined for an 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 for annotations of ontologies, 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 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 = ( N_{DT} , N_{LS} , N_{FS} , ⋅ ^{DT} , ⋅ ^{LS} , ⋅ ^{FS} ) with the following components.
- N_{DT} is a set of datatypes that does not contain the datatype rdfs:Literal.
- N_{LS} is a function that assigns to each datatype DT ∈ N_{DT} a set N_{LS}(DT) of strings called lexical values. The set N_{LS}(DT) is called the lexical space of DT.
- N_{FS} is a function that assigns to each datatype DT ∈ N_{DT} a set N_{FS}(DT) of pairs 〈 F v 〉, where F is a constraining facet and v is an arbitrary object called a value. The set N_{FS}(DT) is called the facet space of DT.
- For each datatype DT ∈ N_{DT}, the interpretation function ⋅ ^{DT} assigns to DT a set (DT)^{DT} called the value space of DT.
- For each datatype DT ∈ N_{DT} and each lexical value LV ∈ N_{LS}(DT), the interpretation function ⋅ ^{LS} assigns to the pair 〈 LV DT 〉 a data value (〈 LV DT 〉)^{LS} ∈ (DT)^{DT}.
- For each datatype DT ∈ N_{DT} and each pair 〈 F v 〉 ∈ N_{FS}(DT), the interpretation function ⋅ ^{FS} assigns to 〈 F v 〉 a facet value (〈 F v 〉)^{FS} ⊆ (DT)^{DT}.
A vocabulary V = ( V_{C} , V_{OP} , V_{DP} , V_{I} , V_{DT} , V_{LT} , V_{FA} ) over a datatype map D is a 7-tuple consisting of the following elements:
- V_{C} 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.
- V_{OP} 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.
- V_{DP} 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:bttomDataProperty.
- V_{I} is a set of individuals (named and anonymous) as defined in the OWL 2 Specification [OWL 2 Specification].
- V_{DT} is the set of all datatypes of D extended with the datatype rdfs:Literal; that is, V_{DT} = N_{DT} ∪ { rdfs:Literal }.
- V_{LT} is a set of literals LV^^DT for each datatype DT ∈ N_{DT} and each lexical value LV ∈ N_{LS}(DT).
- V_{FA} is the set of pairs 〈 F lt 〉 for each constraining facet F, datatype DT ∈ N_{DT}, and literal lt ∈ V_{LT} such that 〈 F (〈 LV DT_{1} 〉)^{LS} 〉 ∈ N_{FS}(DT), where LV is the lexical value of lt and DT_{1} 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;
- PE denotes an object property or 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 Int = ( Δ_{Int} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) for D and V is a 9-tuple with the following structure.
- Δ_{Int} is a nonempty set called the object domain.
- Δ_{D} is a nonempty set disjoint with Δ_{Int} called the data domain such that (DT)^{DT} ⊆ Δ_{D} for each datatype DT ∈ V_{DT}.
- ⋅ ^{C} is the class interpretation function that assigns to each class C ∈ V_{C} a subset (C)^{C} ⊆ Δ_{Int} such that
- (owl:Thing)^{C} = Δ_{Int} and
- (owl:Nothing)^{C} = ∅.
- ⋅ ^{OP} is the object property interpretation function that assigns to each object property OP ∈ V_{OP} a subset (OP)^{OP} ⊆ Δ_{Int} × Δ_{Int} such that
- (owl:topObjectProperty)^{OP} = Δ_{Int} × Δ_{Int} and
- (owl:bottomObjectProperty)^{OP} = ∅.
- ⋅ ^{DP} is the data property interpretation function that assigns to each data property DP ∈ V_{DP} a subset (DP)^{DP} ⊆ Δ_{Int} × Δ_{D} such that
- (owl:topDataProperty)^{DP} = Δ_{Int} × Δ_{D} and
- (owl:bottomDataProperty)^{DP} = ∅.
- ⋅ ^{I} is the individual interpretation function that assigns to each individual a ∈ V_{I} an element (a)^{I} ∈ Δ_{Int}.
- ⋅ ^{DT} is the datatype interpretation function that is the same as in D for all datatypes DT ∈ N_{DT} and is extended to rdfs:Literal by setting
- (rdfs:Literal)^{DT} = Δ_{D}.
- ⋅ ^{LT} is the literal interpretation function that is defined as (lt)^{LT} = (〈 LV DT 〉)^{LS} for each lt ∈ V_{LT}, where LV is the lexical value 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 〉 ∈ V_{FA}.
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.
Object Property Expression | Interpretation ⋅ ^{OP} |
---|---|
InverseOf( 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, a set (DT)^{DT} ⊆ Δ_{D}. Data ranges, however, can be n-ary, as this allows implementations to extend OWL 2 with built-in operations such as comparisons or arithmetic. An n-ary data range DR is interpreted as an n-ary relation (DR)^{DT} over Δ_{D}.
Data Range | Interpretation ⋅ ^{DT} |
---|---|
IntersectionOf( DR_{1} ... DR_{n} ) | (DR_{1})^{DT} ∩ ... ∩ (DR_{n})^{DT} |
UnionOf( DR_{1} ... DR_{n} ) | (DR_{1})^{DT} ∪ ... ∪ (DR_{n})^{DT} |
ComplementOf( DR ) | (Δ_{D})^{n} \ (DR)^{DT} where n is the arity of DR |
OneOf( lt_{1} ... lt_{n} ) | { (lt_{1})^{LT} , ... , (lt_{n})^{LT} } |
DatatypeRestriction( DT F_{1} lt_{1} ... F_{n} lt_{n} ) | (DT)^{DT} ∩ (〈 F_{1} lt_{1} 〉)^{FA} ∩ ... ∩ (〈 F_{n} lt_{n} 〉)^{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.
Class Expression | Interpretation ⋅ ^{C} |
---|---|
IntersectionOf( CE_{1} ... CE_{n} ) | (CE_{1})^{C} ∩ ... ∩ (CE_{n})^{C} |
UnionOf( CE_{1} ... CE_{n} ) | (CE_{1})^{C} ∪ ... ∪ (CE_{n})^{C} |
ComplementOf( CE ) | Δ_{Int} \ (CE)^{C} |
OneOf( a_{1} ... a_{n} ) | { (a_{1})^{I} , ... , (a_{n})^{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} } |
HasSelf( 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( DPE_{1} ... DPE_{n} DR ) | { x | ∃ y_{1}, ... , y_{n} : 〈 x , y_{k} 〉 ∈ (DPE_{k})^{DP} for each 1 ≤ k ≤ n and 〈 y_{1} , ... , y_{n} 〉 ∈ (DR)^{DT} } |
AllValuesFrom( DPE_{1} ... DPE_{n} DR ) | { x | ∀ y_{1}, ... , y_{n} : 〈 x , y_{k} 〉 ∈ (DPE_{k})^{DP} for each 1 ≤ k ≤ n imply 〈 y_{1} , ... , y_{n} 〉 ∈ (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 } |
2.3 Satisfaction in an Interpretation
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 the condition in the tables below for the axiom. Satisfaction of axioms in Int is defined w.r.t. O because satisfaction of key axioms uses the following function:
ISNAMED_{O}(x) = true for x ∈ Δ_{Int} 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 Int w.r.t. O is defined as shown in Table 5.
Axiom | Condition |
---|---|
SubClassOf( CE_{1} CE_{2} ) | (CE_{1})^{C} ⊆ (CE_{2})^{C} |
EquivalentClasses( CE_{1} ... CE_{n} ) | (CE_{j})^{C} = (CE_{k})^{C} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointClasses( CE_{1} ... CE_{n} ) | (CE_{j})^{C} ∩ (CE_{k})^{C} = ∅ for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
DisjointUnion( C CE_{1} ... CE_{n} ) | (C)^{C} = (CE_{1})^{C} ∪ ... ∪ (CE_{n})^{C} and (CE_{j})^{C} ∩ (CE_{k})^{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 Int w.r.t. O is defined as shown in Table 6.
Axiom | Condition |
---|---|
SubPropertyOf( OPE_{1} OPE_{2} ) | (OPE_{1})^{OP} ⊆ (OPE_{2})^{OP} |
SubPropertyOf( PropertyChain( OPE_{1} ... OPE_{n} ) OPE ) | ∀ y_{0} , ... , y_{n} : 〈 y_{0} , y_{1} 〉 ∈ (OPE_{1})^{OP} and ... and 〈 y_{n-1} , y_{n} 〉 ∈ (OPE_{n})^{OP} imply 〈 y_{0} , y_{n} 〉 ∈ (OPE)^{OP} |
EquivalentProperties( OPE_{1} ... OPE_{n} ) | (OPE_{j})^{OP} = (OPE_{k})^{OP} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointProperties( OPE_{1} ... OPE_{n} ) | (OPE_{j})^{OP} ∩ (OPE_{k})^{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( OPE_{1} OPE_{2} ) | (OPE_{1})^{OP} = { 〈 x , y 〉 | 〈 y , x 〉 ∈ (OPE_{2})^{OP} } |
FunctionalProperty( OPE ) | ∀ x , y_{1} , y_{2} : 〈 x , y_{1} 〉 ∈ (OPE)^{OP} and 〈 x , y_{2} 〉 ∈ (OPE)^{OP} imply y_{1} = y_{2} |
InverseFunctionalProperty( OPE ) | ∀ x_{1} , x_{2} , y : 〈 x_{1} , y 〉 ∈ (OPE)^{OP} and 〈 x_{2} , y 〉 ∈ (OPE)^{OP} imply x_{1} = x_{2} |
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} |
2.3.3 Data Property Expression Axioms
Satisfaction of OWL 2 data property expression axioms in Int w.r.t. O is defined as shown in Table 7.
Axiom | Condition |
---|---|
SubPropertyOf( DPE_{1} DPE_{2} ) | (DPE_{1})^{DP} ⊆ (DPE_{2})^{DP} |
EquivalentProperties( DPE_{1} ... DPE_{n} ) | (DPE_{j})^{DP} = (DPE_{k})^{DP} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DisjointProperties( DPE_{1} ... DPE_{n} ) | (DPE_{j})^{DP} ∩ (DPE_{k})^{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 , y_{1} , y_{2} : 〈 x , y_{1} 〉 ∈ (DPE)^{DP} and 〈 x , y_{2} 〉 ∈ (DPE)^{DP} imply y_{1} = y_{2} |
2.3.4 Keys
Satisfaction of keys in Int w.r.t. O is defined as shown in Table 8.
Axiom | Condition |
---|---|
HasKey( CE PE_{1} ... PE_{n} ) | ∀ x , y , z_{1} , ... , z_{n} : if ISNAMED_{O}(x) and ISNAMED_{O}(y) and x ∈ (CE)^{C} and y ∈ (CE)^{C} and for each 1 ≤ i ≤ n, if PE_{i} is an object property, then 〈 x , z_{i} 〉 ∈ (PE_{i})^{OP} and 〈 y , z_{i} 〉 ∈ (PE_{i})^{OP} and ISNAMED_{O}(z_{i}), and if PE_{i} is a data property, then 〈 x , z_{i} 〉 ∈ (PE_{i})^{DP} and 〈 y , z_{i} 〉 ∈ (PE_{i})^{DP} then x = y |
2.3.5 Assertions
Satisfaction of OWL 2 assertions in Int w.r.t. O is defined as shown in Table 9.
Axiom | Condition |
---|---|
SameIndividual( a_{1} ... a_{n} ) | (a_{j})^{I} = (a_{k})^{I} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n |
DifferentIndividuals( a_{1} ... a_{n} ) | (a_{j})^{I} ≠ (a_{k})^{I} for each 1 ≤ j ≤ n and each 1 ≤ k ≤ n such that j ≠ k |
ClassAssertion( CE a ) | (a)^{I} ∈ (CE)^{C} |
PropertyAssertion( OPE a_{1} a_{2} ) | 〈 (a_{1})^{I} , (a_{2})^{I} 〉 ∈ (OPE)^{OP} |
NegativePropertyAssertion( OPE a_{1} a_{2} ) | 〈 (a_{1})^{I} , (a_{2})^{I} 〉 ∉ (OPE)^{OP} |
PropertyAssertion( DPE a lt ) | 〈 (a)^{I} , (lt)^{LT} 〉 ∈ (DPE)^{DP} |
NegativePropertyAssertion( DPE a lt ) | 〈 (a)^{I} , (lt)^{LT} 〉 ∉ (DPE)^{DP} |
2.3.6 Ontologies
An interpretation 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.
2.4 Models
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_{1} = ( Δ_{Int} , Δ_{D} , ⋅ ^{C} , ⋅ ^{OP} , ⋅ ^{DP} , ⋅ ^{I1} , ⋅ ^{DT} , ⋅ ^{LT} , ⋅ ^{FA} ) exists such that ⋅ ^{I1} coincides with ⋅ ^{I} on all named individuals and Int_{1} 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_{1} that satisfies O.
2.5 Inference Problems
In this section variables are a new kind of syntactic construct, disjoint from the syntactic constructs of OWL 2.
Let D be a datatype map and V a vocabulary over D. Furthermore, let O and O_{1} be OWL 2 ontologies, CE, CE_{1}, and CE_{2} 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
∃ x_{1} , ... , x_{n} , y_{1} , ... , y_{m} : [ A_{1} ∧ ... ∧ A_{k} ]
where each A_{i} 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 x_{j}, and u a literal or some variable y_{j}.
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_{1} w.r.t. D if every model of O w.r.t. D and V is also a model of O_{1} w.r.t. D and V.
Ontology Equivalence: O and O_{1} are equivalent w.r.t. D if O entails O_{1} w.r.t. D and O_{1} entails O w.r.t. D.
Ontology Equisatisfiability: O and O_{1} are equisatisfiable w.r.t. D if O is satisfiable w.r.t. D if and only if O_{1} 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: CE_{1} is subsumed by a class expression CE_{2} w.r.t. O and D if (CE_{1})^{C} ⊆ (CE_{2})^{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, making the usual changes needed to account for quantification and variables.
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 O_{1}, CE, CE_{1}, and CE_{2} can contain only object property expressions that are simple in the axiom closure Ax of O.
For ontology equivalence to be decidable, O_{1} 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 Semantics from the Datatype Map
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:
- One can interpret an OWL 2 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 reasoners can provide datatypes not explicitly mentioned in this specification without fear that this will change the semantics of OWL 2 ontologies not using these datatypes.
Theorem DS1. Let O_{1} and O_{2} be OWL 2 ontologies over a vocabulary V and D = ( N_{DT} , N_{LS} , N_{FS} , ⋅ ^{DT} , ⋅ ^{LS} , ⋅ ^{FS} ) a datatype map such that each datatype mentioned in O_{1} and O_{2} is either rdfs:Literal or it occurs in N_{DT}. Furthermore, let D' = ( N_{DT}' , N_{LS}' , N_{FS}' , ⋅ ^{DT '} , ⋅ ^{LS '} , ⋅ ^{FS '} ) be a datatype map such that N_{DT} ⊆ N_{DT}', N_{LS}(DT) = N_{LS}'(DT), and N_{FS}(DT) = N_{FS}'(DT) for each DT ∈ N_{DT}, and ⋅ ^{DT '}, ⋅ ^{LS '}, and ⋅ ^{FS '} are extensions of ⋅ ^{DT}, ⋅ ^{LS}, and ⋅ ^{FS}, respectively. Then, O_{1} entails O_{2} w.r.t. D if and only if O_{1} entails O_{2} w.r.t. D'.
Proof. Without loss of generality, one can assume O_{1} and O_{2} 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 V exists such that O_{1} is and O_{2} is not satisfied in Int if and only if an interpretation Int' w.r.t. D' and V exists such that O_{1} is and O_{2} 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 O_{1} is and O_{2} is not satisfied in Int. Let Int' = ( Δ_{Int} , Δ_{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 N_{DT}' \ N_{DT},
- ⋅ ^{C '} coincides with ⋅ ^{C} on all classes, and
- ⋅ ^{DP '} coincides with ⋅ ^{DP} on all data properties apart from owl:topDataProperty.
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 owl:topDataProperty property can occur in O_{1} and O_{2} only in tautologies. The interpretation of all other data properties is the same in Int and Int', so (CE)^{C} = (CE)^{C '} for each class expression CE occurring in O_{1} and O_{2}. Therefore, O_{1} is and O_{2} is not satisfied in Int'. QED
4 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, and Vipul Kashyap.
5 References
- [Description Logics]
- The Description Logic Handbook. Franz Baader, Diego Calvanese, Deborah McGuinness, Daniele Nardi, Peter Patel-Schneider, Editors. Cambridge University Press, 2003; and Description Logics Home Page.
- [OWL 2 Specification]
- OWL 2 Web Ontology Language: Structural Specification and Functional-Style Syntax. Boris Motik, Peter F. Patel-Schneider, and Bijan Parsia, eds., 2008
- [OWL 2 Profiles]
- OWL 2 Web Ontology Language: Profiles. Boris Motik, Bernardo Cuenca Grau, Ian Horrocks, Zhe Wu, Achille Fokoue, Carsten Lutz, eds., 2008
- [OWL Abstract Syntax and Semantics]
- OWL Web Ontology Language: Semantics and Abstract Syntax. Peter F. Patel-Schneider, Pat Hayes, and Ian Horrocks, Editors, W3C Recommendation, 10 February 2004.
- [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.
- [RFC-4646]
- RFC 4646 - Tags for Identifying Languages. M. Phillips and A. Davis. IETF, September 2006, http://www.ietf.org/rfc/rfc4646.txt. Latest version is available as BCP 47, (details).