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 36 documents:
These First Public Working Drafts are based closely onSince the OWL 1.1 Submission , a set of documents developed outside of W3C as proposed refinements and extensions toprevious Working Draft (dated 8 January 2008),
the W3C's 2004 OWL Recommendation . A number of features of OWL 1.1 are still under consideration byonly change is the OWL Working Group. Future versions of these documents may modify or drop descriptions of some features, or add specificationname of new features. Where specific issues have been identified on whichthe
Working Group intendslanguage, from "OWL 1.1" to make a decision, relevant parts of this document have been labeled with an "Editor's Note". Although the WG aims to maximise backwards compatibility with OWL 1.0, such compatibility cannot be guaranteed in all cases."OWL 2". Since the
Workinggroup is publishing these drafts for public comment in orderthree new Working Drafts, and the name
has changed, it decided to informpublish the ongoing decision making process.complete set with
consistent names.
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 |
Editor's Note: See Issue-72 (Annotation Semantics).
Editor's Note: See Issue 63 (OWL Full Semantics).
Editor's Note: See Issue 69 (punning).
This document defines the formal semantics of OWL 1.1.2. The
semantics given here follows the principles for defining the
semantics of description logics [Description Logics]
and is compatible with the description logic SROIQ presented
in [SROIQ].
Unfortunately, the definition of SROIQ given in
[SROIQ] does not
provide for datatypes and metamodeling. Therefore, the semantics of
OWL 1.12 is defined in a direct model-theoretic way, by interpreting
the constructs of the functional-style syntax from [OWL 1.12 Specification].
For the constructs available in SROIQ, the semantics of
SROIQ trivially corresponds to the one defined in this
document.
OWL 1.12 does not have an RDF-compatible semantics. Ontologies
expressed in OWL RDF are given semantics by converting then into
the functional-style syntax and interpreting the result as
specified in this document.
OWL 1.12 allows for annotations of ontologies and ontology entities
(classes, properties, and individuals) and ontology axioms.
Annotations, however, have no semantic meaning in OWL 1.12 and are
ignored in this document. Definitions in OWL 1.12 similarly have no
semantics. Constructs only used in annotations and definitions,
like ObjectProperty, therefore do not
show up in this document.
Since OWL 1.12 is an extension of OWL DL, this document also
provides a formal semantics for OWL Lite and OWL DL and it is
equivalent to the definition given in [OWL Abstract
Syntax and Semantics].
Editor's Note: See Issue-73 (infinite universe ).
A vocabulary (or signature) V = ( NC , NPo , NPd , NI , ND , NV ) is a 6-tuple where
Since OWL 1.12 allows punning [Metamodeling] in the
signature, we do not require the sets NC ,
NPo , NPd , NI , ND ,
and NV to be pair-wise disjoint. Thus, the same name can
be used in an ontology to denote a class, a datatype, a property
(object or data), an individual, and a constant. The set
ND is defined as it is because a datatype is
defined by its name and the arity, and such a definition allows one
to reuse the same name with different arities.
The semantics of OWL 1.12 is defined with respect to a concrete
domain, which is a tuple D = ( ΔD , .D
) where
The set of datatypes ND in each OWL 1.12
vocabulary must include a unary datatype rdfs:Literal
interpreted as ΔD; furthermore, it must also
include the following unary datatypes: xsd:string,
xsd:boolean,
xsd:decimal,
xsd:float,
xsd:double,
xsd:dateTime,
xsd:time,
xsd:date,
xsd:gYearMonth, xsd:gYear,
xsd:gMonthDay,
xsd:gDay,
xsd:gMonth,
xsd:hexBinary,
xsd:base64Binary, xsd:anyURI,
xsd:normalizedString, xsd:token,
xsd:language,
xsd:NMTOKEN,
xsd:Name,
xsd:NCName,
xsd:integer,
xsd:nonPositiveInteger,
xsd:negativeInteger, xsd:long,
xsd:int,
xsd:short,
xsd:byte,
xsd:nonNegativeInteger,
xsd:unsignedLong,
xsd:unsignedInt,
xsd:unsignedShort,
xsd:unsignedByte, and
xsd:positiveInteger. These datatypes, as well as the
well-formed constants from NV, are interpreted as
specified in [XML Schema Datatypes]. (Note that the value spaces of
primitive XML Schema Datatypes are disjoint, so "2"^^xsd:decimalD is different from
"2"^^xsd:float"D.)
The set ΔD is a fixed set that must be large enough; that is, it must contain the extension of each datatype from ND and, apart from that, an infinite number of other objects. Such a definition is ambiguous, as it does not uniquely single out a particular set ΔD; however, the choice of the actual set is not actually relevant for the definition of the semantics, as long as it contains the interpretations of all datatypes that one can "reasonably think of." This allows the implementations to support datatypes other than the ones mentioned in the previous paragraphs without affecting the semantics.
Given a vocabulary V and a concrete domain D, an interpretation I = ( ΔI , .Ic , .Ipo , .Ipd , .Ii ) is a 5-tuple where
We extend the object interpretation function .Ipo to object property expressions as shown in Table 1.
Object Property Expression | Interpretation |
---|---|
InverseObjectProperty(R) | { ( x , y ) | ( y , x ) ∈ RIpo } |
We extend the interpretation function .D to data ranges as shown in Table 2.
Data Range | Interpretation |
---|---|
DataOneOf(v1 ... vn) | { v1D , ... , vnD } |
DataComplementOf(DR) | ( ΔD )n \ DRD where n is the arity of DR |
DatatypeRestriction(DR f v) |
the n-ary relation over ΔD obtained by
applying the facet f with value v |
We extend the class interpretation function .Ic to descriptions as shown in Table 3. With #S we denote the number of elements in a set S.
Description | Interpretation |
---|---|
owl:Thing | ΔI |
owl:Nothing | empty set |
ObjectComplementOf(C) | ΔI \ CIc |
ObjectIntersectionOf(C1 ... Cn) | C1Ic ∩ ... ∩ CnIc |
ObjectUnionOf(C1 ... Cn) | C1Ic ∪ ... ∪ CnIc |
ObjectOneOf(a1 ... an) | { a1Ii , ... , anIi } |
ObjectSomeValuesFrom(R C) | { x | ∃ y |
ObjectAllValuesFrom(R C) | { x | ∀ y |
ObjectHasValue(R a) | { x | ( x, aIi ) ∈ RIpo } |
ObjectExistsSelf(R) | { x | ( x, x ) ∈ RIpo } |
ObjectMinCardinality(n R C) | { x | #{ y | ( x, y ) ∈ RIpo and y ∈ CIc } ≥ n } |
ObjectMaxCardinality(n R C) | { x | #{ y | ( x, y ) ∈ RIpo and y ∈ CIc } ≤ n } |
ObjectExactCardinality(n R C) | { x | #{ y | ( x, y ) ∈ RIpo and y ∈ CIc } = n } |
DataSomeValuesFrom(U1 ... Un DR) | { x | ∃ y1, ...,
yn |
DataAllValuesFrom(U1 ... Un DR) | { x | ∀ y1, ...,
yn |
DataHasValue(U v) | { x | ( x, vD ) ∈ UIpd } |
DataMinCardinality(n U DR) | { x | #{ y | ( x, y ) ∈ UIpd and y ∈ DRD } ≥ n } |
DataMaxCardinality(n U DR) | { x | #{ y | ( x, y ) ∈ UIpd and y ∈ DRD } ≤ n } |
DataExactCardinality(n U DR) | { x | #{ y | ( x, y ) ∈ UIpd and y ∈ DRD } = n } |
Satisfaction of OWL 1.12 axioms in an interpretation I is
defined as shown in Table 4. With o we denote the
composition of binary relations.
Axiom | Condition |
---|---|
SubClassOf(C D) | CIc ⊆ DIc |
EquivalentClasses(C1 ... Cn) | CjIc = CkIc for each 1 ≤ j , k ≤ n |
DisjointClasses(C1 ... Cn) | CjIc ∩ CkIc is empty for each 1 ≤ j , k ≤ n and j ≠ k |
DisjointUnion(A C1 ... Cn) | AIc = C1Ic ∪ ... ∪ CnIc and CjIc ∩ CkIc is empty for each 1 ≤ j , k ≤ n and j ≠ k |
SubObjectPropertyOf(R S) | RIpo ⊆ SIpo |
SubObjectPropertyOf(SubObjectPropertyChain(R1 ... Rn) S) | R1Ipo o ... o RnIpo ⊆ SIpo |
EquivalentObjectProperties(R1 ... Rn) | RjIpo = RkIpo for each 1 ≤ j , k ≤ n |
DisjointObjectProperties(R1 ... Rn) | RjIpo ∩ RkIpo is empty for each 1 ≤ j , k ≤ n and j ≠ k |
ObjectPropertyDomain(R C) | { x | ∃ |
ObjectPropertyRange(R C) | { y | ∃ |
InverseObjectProperties(R S) | RIpo = { ( x , y ) | ( y , x ) ∈ SIpo } |
FunctionalObjectProperty(R) | ( x , y1 ) ∈ RIpo and ( x , y2 ) ∈ RIpo imply y1 = y2 |
InverseFunctionalObjectProperty(R) | ( x1 , y ) ∈ RIpo and ( x2 , y ) ∈ RIpo imply x1 = x2 |
ReflexiveObjectProperty(R) | x ∈ ΔI implies ( x , x ) ∈ RIpo |
IrreflexiveObjectProperty(R) | x ∈ ΔI implies ( x , x ) is not in RIpo |
SymmetricObjectProperty(R) | ( x , y ) ∈ RIpo implies ( y , x ) ∈ RIpo |
AsymmetricObjectProperty(R) | ( x , y ) ∈ RIpo implies ( y , x ) is not in RIpo |
TransitiveObjectProperty(R) | RIpo o RIpo ⊆ RIpo |
SubDataPropertyOf(U V) | UIpd ⊆ VIpd |
EquivalentDataProperties(U1 ... Un) | UjIpd = UkIpd for each 1 ≤ j , k ≤ n |
DisjointDataProperties(U1 ... Un) | UjIpd ∩ UkIpd is empty for each 1 ≤ j , k ≤ n and j ≠ k |
DataPropertyDomain(U C) | { x | ∃ |
DataPropertyRange(U DR) | { y | ∃ |
FunctionalDataProperty(U) | ( x , y1 ) ∈ UIpd and ( x , y2 ) ∈ UIpd imply y1 = y2 |
SameIndividual(a1 ... an) | ajIi = akIi for each 1 ≤ j , k ≤ n |
DifferentIndividuals(a1 ... an) | ajIi ≠ akIi for each 1 ≤ j , k ≤ n and j ≠ k |
ClassAssertion(a C) | aIi ∈ CIc |
ObjectPropertyAssertion(R a b) | ( aIi , bIi ) ∈ RIpo |
NegativeObjectPropertyAssertion(R a b) | ( aIi , bIi ) is not in RIpo |
DataPropertyAssertion(U a v) | ( aIi , vD ) ∈ UIpd |
NegativeDataPropertyAssertion(U a v) | ( aIi , vD ) is not in UIpd |
Let O be an OWL 1.12 ontology with vocabulary V.
O is consistent if an interpretation I exists
that satisfies all the axioms of the axiom closure of O (the
axiom closure of O is defined in [OWL 1.12
Specification]); such I is then called a
model of O. A description C is satisfiable
w.r.t. O if there is a model I of O such that
CIc is not empty. O entails an OWL
1.12 ontology O' with vocabulary V if every model of
O is also a model of O'; furthermore, O and
O' are equivalent if O entails O' and
O' entails O.