Movatterモバイル変換

OWL 2 Web Ontology Language
Direct Semantics (Second Edition)

W3C Recommendation 11 December 2012

This version:

http://www.w3.org/TR/2012/REC-owl2-direct-semantics-20121211/

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/2012/PER-owl2-direct-semantics-20121018/

Editors:

Boris Motik, University of Oxford

Peter F. Patel-Schneider, Nuance Communications

Bernardo Cuenca Grau, University of Oxford

Contributors: (in alphabetical order)

Ian Horrocks, University of Oxford

Bijan Parsia, University of Manchester

Uli Sattler, University of Manchester

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

Acolor-coded version of this document showing changes made since the previous version is also available.

This document is also available in these non-normative formats:PDF version.

See alsotranslations.

Copyright © 2012W3C^® (MIT,ERCIM,Keio), All Rights Reserved. W3Cliability,trademark anddocument use rules apply.

Abstract

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 theW3C technical reports index at http://www.w3.org/TR/.

Summary of Changes

Please Send Comments

Please send any comments topublic-owl-comments@w3.org (public archive). Although work on this document by theOWL Working Group is complete, comments may be addressed in theerrata or in future revisions. Open discussion among developers is welcome atpublic-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 the5 February 2004 W3C Patent Policy. W3C maintains apublic list of any patent disclosures made in connection with the deliverables of the group; that page also includes instructions for disclosing a patent.

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 logicSROIQ [SROIQ]. As the definition ofSROIQ 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 toSROIQ. For the constructs available inSROIQ, the semantics ofSROIQ 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

Adatatype map, formalizingdatatype maps from the OWL 2 Specification [OWL 2 Specification], is a 6-tupleD = (N_DT ,N_LS ,N_FS ,⋅ ^DT ,⋅ ^LS ,⋅ ^FS ) with the following components:

• N_DT is a set of datatypes (more precisely, names of datatypes) that does not contain the datatyperdfs:Literal.
• N_LS is a function that assigns to each datatypeDT ∈N_DT a setN_LS(DT) of strings calledlexical forms. The setN_LS(DT) is called thelexical space ofDT.
• N_FS is a function that assigns to each datatypeDT ∈N_DT a setN_FS(DT) of pairs (F ,v ), whereF is aconstraining facet andv is an arbitrary data value called theconstraining value. The setN_FS(DT) is called thefacet space ofDT.
• For each datatypeDT ∈N_DT, theinterpretation function⋅ ^DT assigns toDT a set(DT)^DT called thevalue space ofDT.
• For each datatypeDT ∈N_DT and each lexical formLV ∈N_LS(DT), theinterpretation function⋅ ^LS assigns to the pair (LV ,DT ) adata value (LV ,DT )^LS ∈(DT)^DT.
• For each datatypeDT ∈N_DT and each pair (F ,v ) ∈N_FS(DT), theinterpretation function⋅ ^FS assigns to (F ,v ) the set (F ,v )^FS ⊆(DT)^DT.

The set of datatypesN_DT of a datatype mapD is not required to contain all datatypes from theOWL 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 datatypeDT from theOWL 2 datatype map, thenN_LS(DT),N_FS(DT),(DT)^DT, (LV ,DT )^LS for eachLV ∈N_LS(DT), and (F ,v )^FS for each (F ,v ) ∈N_FS(DT) are required to coincide with the definitions forDT in theOWL 2 datatype map.

AvocabularyV = (V_C ,V_OP ,V_DP ,V_I ,V_DT ,V_LT ,V_FA ) over a datatype mapD is a 7-tuple consisting of the following elements:

• V_C is a set ofclasses as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the classesowl:Thing andowl:Nothing.
• V_OP is a set ofobject properties as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the object propertiesowl:topObjectProperty andowl:bottomObjectProperty.
• V_DP is a set ofdata properties as defined in the OWL 2 Specification [OWL 2 Specification], containing at least the data propertiesowl:topDataProperty andowl:bottomDataProperty.
• V_I is a set ofindividuals (named and anonymous) as defined in the OWL 2 Specification [OWL 2 Specification].
• V_DT is a set containing all datatypes ofD, the datatyperdfs:Literal, and possibly other datatypes; that is,N_DT ∪ {rdfs:Literal } ⊆V_DT.
• V_LT is a set ofliteralsLV^^DT for each datatypeDT ∈N_DT and each lexical formLV ∈N_LS(DT).
• V_FA is the set of pairs (F ,lt ) for each constraining facetF, datatypeDT ∈N_DT, and literallt ∈V_LT such that (F , (LV ,DT₁ )^LS ) ∈N_FS(DT), whereLV is the lexical form oflt andDT₁ is the datatype oflt.

Given a vocabularyV, 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 mapD and a vocabularyV overD, aninterpretationI = (Δ_I ,Δ_D ,⋅ ^C ,⋅ ^OP ,⋅ ^DP ,⋅ ^I ,⋅ ^DT ,⋅ ^LT ,⋅ ^FA ,NAMED ) forD andV is a 10-tuple with the following structure:

• Δ_I is a nonempty set called theobject domain.
• Δ_D is a nonempty set disjoint withΔ_I called thedata domain such that(DT)^DT ⊆Δ_D for each datatypeDT ∈V_DT.
• ⋅ ^C is theclass interpretation function that assigns to each classC ∈ V_C a subset(C)^C ⊆Δ_I such that
  • (owl:Thing)^C =Δ_I and
  • (owl:Nothing)^C = ∅.
• ⋅ ^OP is theobject property interpretation function that assigns to each object propertyOP ∈ V_OP a subset(OP)^OP ⊆Δ_I ×Δ_I such that
  • (owl:topObjectProperty)^OP =Δ_I ×Δ_I and
  • (owl:bottomObjectProperty)^OP = ∅.
• ⋅ ^DP is thedata property interpretation function that assigns to each data propertyDP ∈ V_DP a subset(DP)^DP ⊆Δ_I ×Δ_D such that
  • (owl:topDataProperty)^DP =Δ_I ×Δ_D and
  • (owl:bottomDataProperty)^DP = ∅.
• ⋅ ^I is theindividual interpretation function that assigns to each individuala ∈ V_I an element(a)^I ∈Δ_I.
• ⋅ ^DT is thedatatype interpretation function that assigns to each datatypeDT ∈ V_DT a subset(DT)^DT ⊆Δ_D such that
  • ⋅ ^DT is the same as inD for each datatypeDT ∈N_DT, and
  • (rdfs:Literal)^DT =Δ_D.
• ⋅ ^LT is theliteral interpretation function that is defined as(lt)^LT = (LV ,DT )^LS for eachlt ∈V_LT, whereLV is the lexical form oflt andDT is the datatype oflt.
• ⋅ ^FA is thefacet interpretation function that is defined as (F ,lt )^FA = (F ,(lt)^LT )^FS for each (F ,lt ) ∈V_FA.
• NAMED is a subset ofΔ_I such that(a)^I ∈NAMED for each named individuala ∈V_I.

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.

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 datatypeDT 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 forn-ary data ranges, the syntax of OWL 2 provides a "hook" allowing implementations to introduce extensions such as comparisons and arithmetic. Ann-ary data rangeDR is interpreted as ann-ary relation(DR)^DT overΔ_D — that is, as a set(DT)^DT ⊆(Δ_D)ⁿ

2.2.3 Class Expressions

The class interpretation function⋅ ^C is extended to class expressions as shown in Table 4. ForS a set,#S denotes the number of elements inS.

2.3 Satisfaction in an Interpretation

An axiom or an ontology issatisfied in an interpretationI = (Δ_I ,Δ_D ,⋅ ^C ,⋅ ^OP ,⋅ ^DP ,⋅ ^I ,⋅ ^DT ,⋅ ^LT ,⋅ ^FA ,NAMED ) if the appropriate condition from the following sections holds.

2.3.1 Class Expression Axioms

Satisfaction of OWL 2 class expression axioms inI is defined as shown in Table 5.

2.3.2 Object Property Expression Axioms

Satisfaction of OWL 2 object property expression axioms inI is defined as shown in Table 6.

2.3.3 Data Property Expression Axioms

Satisfaction of OWL 2 data property expression axioms inI is defined as shown in Table 7.

2.3.4 Datatype Definitions

Satisfaction of datatype definitions inI is defined as shown in Table 8.

2.3.5 Keys

Satisfaction of keys inI is defined as shown in Table 9.

2.3.6 Assertions

Satisfaction of OWL 2 assertions inI is defined as shown in Table 10.

2.3.7 Ontologies

An OWL 2 ontologyO issatisfied in an interpretationI if all axioms in theaxiom closure ofO (with anonymous individuals standardized apart as described in Section 5.6.2 of the OWL 2 Specification [OWL 2 Specification]) are satisfied inI.

2.4 Models

Given a datatype mapD, an interpretationI = (Δ_I ,Δ_D ,⋅ ^C ,⋅ ^OP ,⋅ ^DP ,⋅ ^I ,⋅ ^DT ,⋅ ^LT ,⋅ ^FA ,NAMED ) forD is amodel of an OWL 2 ontologyO w.r.t.D if an interpretationJ = (Δ_I ,Δ_D ,⋅ ^C ,⋅ ^OP ,⋅ ^DP ,⋅ ^J ,⋅ ^DT ,⋅ ^LT ,⋅ ^FA ,NAMED ) forD exists such that⋅ ^J coincides with⋅ ^I on all named individuals andJ satisfiesO.

Thus, an interpretationI satisfyingO is also a model ofO. In contrast, a modelI ofO may not satisfyO directly; however, by modifying the interpretation of anonymous individuals,I can always be coerced into an interpretationJ that satisfiesO.

2.5 Inference Problems

LetD be a datatype map andV a vocabulary overD. Furthermore, letO andO₁ be OWL 2 ontologies,CE,CE₁, andCE₂ class expressions, anda a named individual, such that all of them refer only to the vocabulary elements inV. Furthermore,variables are symbols that are not contained inV. Finally, aBoolean conjunctive queryQ is a closed formula of the form

where eachA_i is anatom of the formC(s),OP(s,t), orDP(s,u) withC a class,OP an object property,DP a data property,s andt individuals or some variablex_j, andu a literal or some variabley_j.

The following inference problems are often considered in practice.

Ontology Consistency:O isconsistent (orsatisfiable) w.r.t.D if a model ofO w.r.t.D andV exists.

Ontology Entailment:OentailsO₁ w.r.t.D if every model ofO w.r.t.D andV is also a model ofO₁ w.r.t.D andV.

Ontology Equivalence:O andO₁ areequivalent w.r.t.D ifO entailsO₁ w.r.t.D andO₁ entailsO w.r.t.D.

Ontology Equisatisfiability:O andO₁ areequisatisfiable w.r.t.D ifO is satisfiable w.r.t.D if and only ifO₁ is satisfiable w.r.tD.

Class Expression Satisfiability:CE is satisfiable w.r.t.O andD if a modelI = (Δ_I ,Δ_D ,⋅ ^C ,⋅ ^OP ,⋅ ^DP ,⋅ ^I ,⋅ ^DT ,⋅ ^LT ,⋅ ^FA ,NAMED ) ofO w.r.t.D andV exists such that(CE)^C ≠ ∅.

Class Expression Subsumption:CE₁ issubsumed by a class expressionCE₂ w.r.t.O andD if(CE₁)^C ⊆(CE₂)^C for each modelI = (Δ_I ,Δ_D ,⋅ ^C ,⋅ ^OP ,⋅ ^DP ,⋅ ^I ,⋅ ^DT ,⋅ ^LT ,⋅ ^FA ,NAMED ) ofO w.r.t.D andV.

Instance Checking:a is aninstance ofCE w.r.t.O andD if(a)^I ∈(CE)^C for each modelI = (Δ_I ,Δ_D ,⋅ ^C ,⋅ ^OP ,⋅ ^DP ,⋅ ^I ,⋅ ^DT ,⋅ ^LT ,⋅ ^FA ,NAMED ) ofO w.r.t.D andV.

Boolean Conjunctive Query Answering:Q is ananswer w.r.t.O andD ifQ is true in each model ofO w.r.t.D andV 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:

For ontology equivalence to be decidable,O₁ 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 ontologyO do not depend on the choice of a datatype map, as long as the datatype map chosen contains all the datatypes occurring inO. 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 ontologyO by considering only the datatypes explicitly occurring inO.
• When referring to various reasoning problems, the datatype mapD 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. LetO₁ andO₂ be OWL 2 DL ontologies over a vocabularyV andD = (N_DT ,N_LS ,N_FS ,⋅ ^DT ,⋅ ^LS ,⋅ ^FS ) a datatype map such that each datatype mentioned inO₁ andO₂ isrdfs:Literal, a datatype defined in the respective ontology, or it occurs inN_DT. Furthermore, letD' = (N_DT' ,N_LS' ,N_FS' ,⋅ ^DT ' ,⋅ ^LS ' ,⋅ ^FS ' ) be a datatype map such thatN_DT ⊆N_DT',N_LS(DT) =N_LS'(DT), andN_FS(DT) =N_FS'(DT) for eachDT ∈N_DT, and⋅ ^DT ',⋅ ^LS ', and⋅ ^FS ' are extensions of⋅ ^DT,⋅ ^LS, and⋅ ^FS, respectively. Then,O₁ entailsO₂ w.r.t.D if and only ifO₁ entailsO₂ w.r.t.D'.

Proof. Without loss of generality, one can assumeO₁ andO₂ to be in negation-normal form [Description Logics]. Furthermore, since datatype definitions inO₁ andO₂ are acyclic, one can assume that each defined datatype has been recursively replaced with its definition; thus, all datatypes inO₁ andO₂ are fromN_DT ∪ {rdfs:Literal }. The claim of the theorem is equivalent to the following statement: an interpretationI w.r.t.D andV exists such thatO₁ is andO₂ is not satisfied inI if and only if an interpretationI' w.r.t.D' andV exists such thatO₁ is andO₂ is not satisfied inI'. The (⇐) direction is trivial since each interpretationI w.r.t.D' andV is also an interpretation w.r.t.D andV. For the (⇒) direction, assume that an interpretationI = (Δ_I ,Δ_D ,⋅ ^C ,⋅ ^OP ,⋅ ^DP ,⋅ ^I ,⋅ ^DT ,⋅ ^LT ,⋅ ^FA ,NAMED ) w.r.t.D andV exists such thatO₁ is andO₂ is not satisfied inI. LetI' = (Δ_I ,Δ_D' ,⋅ ^C ' ,⋅ ^OP ,⋅ ^DP ' ,⋅ ^I ,⋅ ^DT ' ,⋅ ^LT ' ,⋅ ^FA ' ,NAMED ) be an interpretation such that

• Δ_D' is obtained by extendingΔ_D with the value space of all datatypes inN_DT' \N_DT,
• ⋅ ^C ' coincides with⋅ ^C on all classes, and
• ⋅ ^DP ' coincides with⋅ ^DP on all data properties apart fromowl:topDataProperty.

Clearly,DataComplementOf( DR )^DT ⊆DataComplementOf( DR )^DT ' for each data rangeDR that is either a datatype, a datatype restriction, or an enumerated data range. Theowl:topDataProperty property can occur inO₁ andO₂ only in tautologies. The interpretation of all other data properties is the same inI andI', so(CE)^C =(CE)^C ' for each class expressionCE occurring inO₁ andO₂. Therefore,O₁ is andO₂ is not satisfied inI'. QED

5 Acknowledgments

The starting point for the development of OWL 2 was theOWL1.1 member submission, itself a result of user and developer feedback, and in particular of information gathered during theOWL Experiences and Directions (OWLED) Workshop series. The working group also consideredpostponed issues from theWebOnt 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 toMarkus Krötzsch (FZI),Michael Schneider (FZI) andThomas 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), andAntoine Zimmermann (DERI Galway).We would also like to thank past members of the working group:Jeremy Carroll,Jim Hendler, andVipul Kashyap.

6 References

6.1 Normative References

[OWL 2 Specification]

OWL 2 Web Ontology Language:Structural Specification and Functional-Style Syntax (Second Edition) Boris Motik, Peter F. Patel-Schneider, Bijan Parsia, eds. W3C Recommendation, 11 December 2012,http://www.w3.org/TR/2012/REC-owl2-syntax-20121211/. Latest version available athttp://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 theDescription 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 (Second Edition) Boris Motik, Bernardo Cuenca Grau, Ian Horrocks, Zhe Wu, Achille Fokoue, Carsten Lutz, eds. W3C Recommendation, 11 December 2012,http://www.w3.org/TR/2012/REC-owl2-profiles-20121211/. Latest version available athttp://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.