Model-Theoretic Semantics

- This version:
- http://www.w3.org/submissions/2006/SUBM-owl11-semantics-20061219/
- Latest version:
- http://www.w3.org/submissions/owl11-semantics/
- Authors:
- Bernardo Cuenca Grau, The University of Manchester
- Boris Motik, The University of Manchester
- Contributors:
- Ian Horrocks, The University of Manchester
- Bijan Parsia, The University of Manchester
- Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies
- Ulrike Sattler, The University of Manchester

Copyright © 2006 by the Submitters. This document is available under the W3C Document License. See the W3C Intellectual Rights Notice and Legal Disclaimers for additional information.

OWL 1.1 extends the W3C OWL Web Ontology Language with a small but useful set of features that have been requested by users, for which effective reasoning algorithms are now available, and that OWL tool developers are willing to support. The new features include extra syntactic sugar, additional property and qualified cardinality constructors, extended datatype support, simple metamodeling, and extended annotations. This document provides a model-theoretic semantics for OWL 1.1.

*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 can be found in
the W3C technical reports index
at http://www.w3.org/TR/.*

By publishing this document, W3C acknowledges that the Submitting Members have made a formal Submission request to W3C for discussion. Publication of this document by W3C indicates no endorsement of its content by W3C, nor that W3C has, is, or will be allocating any resources to the issues addressed by it. This document is not the product of a chartered W3C group, but is published as potential input to the W3C Process. A W3C Team Comment has been published in conjunction with this Member Submission. Publication of acknowledged Member Submissions at the W3C site is one of the benefits of W3C Membership. Please consult the requirements associated with Member Submissions of section 3.3 of the W3C Patent Policy. Please consult the complete list of acknowledged W3C Member Submissions.

Please send feedback to public-owl-dev@w3.org, which has a public archive.

This document defines the formal semantics of OWL 1.1. 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.1 is defined in a direct
model-theoretic way, by interpreting the constructs of the functional-style syntax from
[OWL 1.1 Specification].
For the constructs available in *SROIQ*, the semantics of *SROIQ*
trivially corresponds to the one defined in this document.

OWL 1.1 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.1 allows for annotations of ontologies and ontology axioms. Annotations, however, have no semantic meaning in OWL 1.1 and are ignored in this document.

Since OWL 1.1 is an extension of OWL DL, this document also provides a formal semantics for OWL DL and it is equivalent to the definition given in [OWL Abstract Syntax and Semantics].

A *vocabulary* (or *signature*)
*V = ( N _{C} , N_{Po} , N_{Pd} , N_{I} , N_{D} , N_{V} )*
is a 6-tuple where

*N*is a set of_{C}*OWL classes*,*N*is a set of_{Po}*object properties*,*N*is a set of_{Pd}*data properties*,*N*is a set of_{I}*individuals*, and*N*is a set of_{D}*datatypes*each associated with a positive integer*datatype arity*,*N*is a set of well-formed_{V}*constants*.

Since OWL 1.1 allows *punning* [Metamodeling]
in the signature, we do not require the sets N_{C} , N_{Po} , N_{Pd} ,
N_{I} , N_{D} , and N_{V} 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 *N _{D}*
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.1 is defined with respect to a *concrete domain*,
which is a tuple *D = ( Δ _{D} , .^{D} )* where

*Δ*is a fixed set called the_{D}*data domain*,*.*assigns to each constant^{D}*v ∈ N*an element_{V}*v*of^{D}*Δ*, and_{D}*.*assigns to each datatype^{D}*d ∈ N*with arity_{D}*n*an*n*-ary relation*d*over^{D}*Δ*._{D}

The set of datatypes *N _{D}* in each OWL 1.1 vocabulary
must include a unary datatype

The set *Δ _{D}* is a fixed set that must be

Given a vocabulary *V* and a concrete domain *D*, an interpretation
*I = ( Δ _{I} , .^{Ic} , .^{Ipo} , .^{Ipd} , .^{Ii} )* is a 5-tuple where

*Δ*is a nonempty set disjoint with_{I}*Δ*, called the_{D}*object domain*;*.*is the^{Ic}*class interpretation*function that assigns to each OWL class*A ∈ N*a subset_{Ic}*A*of^{Ic}*Δ*;_{I}*.*is the^{Ipo}*object property interpretation*function that assigns to each object property*R ∈ N*a subset_{Po}*R*of^{Ipo}*Δ*;_{I}x Δ_{I}*.*is the^{Ipd}*data property interpretation*function that assigns to each data property*U ∈ N*a subset_{Pd}*U*of^{Ipd}*Δ*;_{I}x Δ_{D}*.*is the^{Ii}*individual interpretation*function that assigns to each individual*a ∈ N*an element_{I}*a*from^{Ii}*Δ*._{I}

We extend the object interpretation function *. ^{Ipo}* to object property expressions as shown in Table 1.

Property | Interpretation |
---|---|

InverseObjectProperty(R) | { ( x , y ) | ( y , x ) ∈ R }^{Ipo} |

We extend the interpretation function *. ^{D}* to data ranges as shown in Table 2.

Data Range | Interpretation |
---|---|

DataOneOf(v_{1} ... v_{n}) |
{ v , ... , _{1}^{D}v }_{n}^{D} |

DataComplementOf(DR) | ( Δ \ _{D} )^{n}DR where ^{D}n is the arity of DR |

DatatypeRestriction(DR f v) | the n-ary relation over Δ obtained by applying the facet _{D}f with value vto the data range DR as specified in [XML Schema Datatypes] |

We extend the class interpretation function *. ^{Ic}* to classes as shown in Table 3.
With

Class | Interpretation |
---|---|

owl:Thing | Δ_{I} |

owl:Nothing | empty set |

ObjectComplementOf(C) | Δ \ _{I}C^{Ic} |

ObjectIntersectionOf(C_{1} ... C_{n}) |
C ∩ ... ∩ _{1}^{Ic}C_{n}^{Ic} |

ObjectUnionOf(C_{1} ... C_{n}) |
C ∪ ... ∪ _{1}^{Ic}C_{n}^{Ic} |

ObjectOneOf(a_{1} ... a_{n}) |
{ a , ... , _{1}^{Ii}a }_{n}^{Ii} |

ObjectSomeValuesFrom(R C) | { x | ∃ y : ( x, y ) ∈ R and ^{Ipo}y ∈ C }^{Ic} |

ObjectAllValuesFrom(R C) | { x | ∀ y : ( x, y ) ∈ R implies ^{Ipo}y ∈ C }^{Ic} |

ObjectHasValue(R a) | { x | ( x, a ∈ ^{Ii} )R }^{Ipo} |

ObjectExistsSelf(R) | { x | ( x, x ) ∈ R }^{Ipo} |

ObjectMinCardinality(n R C) | { x | #{ y | ( x, y ) ∈ R and ^{Ipo}y ∈ C } ≥ n }^{Ic} |

ObjectMaxCardinality(n R C) | { x | #{ y | ( x, y ) ∈ R and ^{Ipo}y ∈ C } ≤ n }^{Ic} |

ObjectExactCardinality(n R C) | { x | #{ y | ( x, y ) ∈ R and ^{Ipo}y ∈ C } = n }^{Ic} |

DatatSomeValuesFrom(U_{1} ... U_{n} DR) |
{ x | ∃ y, ..., _{1}y : _{n}( x, y ∈ _{k} )U for each 1 ≤ _{k}^{Ipd}k ≤ n and ( y ∈ _{1}, ..., y_{n} )DR }^{D} |

DatatAllValuesFrom(U_{1} ... U_{n} DR) |
{ x | ∀ y, ..., _{1}y : _{n}( x, y ∈ _{k} )U for each 1 ≤ _{k}^{Ipd}k ≤ n implies ( y ∈ _{1}, ..., y_{n} )DR }^{D} |

DataHasValue(U v) | { x | ( x, v ∈ ^{D} )U }^{Ipd} |

DataMinCardinality(n U DR) | { x | #{ y | ( x, y ) ∈ U and ^{Ipd}y ∈ DR } ≥ n }^{D} |

DataMaxnCardinality(n U DR) | { x | #{ y | ( x, y ) ∈ U and ^{Ipd}y ∈ DR } ≤ n }^{D} |

DataExactCardinality(n U DR) | { x | #{ y | ( x, y ) ∈ U and ^{Ipd}y ∈ DR } = n }^{D} |

Satisfaction of OWL 1.1 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) | C ⊆ ^{Ic}D^{Ic} |

EquivalentClasses(C_{1} ... C_{n}) |
C = _{j}^{Ic}C for each 1 ≤ _{k}^{Ic}j , k ≤ n |

DisjointClasses(C_{1} ... C_{n}) |
C ∩ _{j}^{Ic}C is empty for each 1 ≤ _{k}^{Ic}j , k ≤ n and j ≠ k |

DisjointUnion(A C_{1} ... C_{n}) |
A = ^{Ic}C ∪ ... ∪ _{1}^{Ic}C and _{n}^{Ic}C ∩ _{j}^{Ic}C is empty for each 1 ≤ _{k}^{Ic}j , k ≤ n and j ≠ k |

SubObjectPropertyOf(R S) | R ⊆ ^{Ipo}S^{Ipo} |

SubObjectPropertyOf(SubObjectPropertyChain(R_{1} ... R_{n}) S) |
R o ... o _{1}^{Ipo}R ⊆ _{n}^{Ipo}S^{Ipo} |

EquivalentObjectProperties(R_{1} ... R_{n}) |
R = _{j}^{Ipo}R for each 1 ≤ _{k}^{Ipo}j , k ≤ n |

DisjointObjectProperties(R_{1} ... R_{n}) |
R ∩ _{j}^{Ipo}R is empty for each 1 ≤ _{k}^{Ipo}j , k ≤ n and j ≠ k |

ObjectPropertyDomain(R C) | { x | ∃ y : (x , y ) ∈ R } ⊆ ^{Ipo}C^{Ic} |

ObjectPropertyRange(R C) | { y | ∃ x : (x , y ) ∈ R } ⊆ ^{Ipo}C^{Ic} |

InverseObjectProperties(R S) | R = { ^{Ipo}( x , y ) | ( y , x ) ∈ S }^{Ipo} |

FunctionalObjectProperty(R) | ( x , y and _{1} ) ∈ R^{Ipo}( x , y imply _{2} ) ∈ R^{Ipo}y_{1} = y_{2} |

InverseFunctionalObjectProperty(R) | ( x and _{1} , y ) ∈ R^{Ipo}( x imply _{2} , y ) ∈ R^{Ipo}x_{1} = x_{2} |

ReflexiveObjectProperty(R) | x ∈ Δ implies _{I}( x , x ) ∈ R^{Ipo} |

IrreflexiveObjectProperty(R) | x ∈ Δ implies _{I}( x , x ) is not in R^{Ipo} |

SymmetricObjectProperty(R) | ( x , y ) ∈ R implies ^{Ipo}( y , x ) ∈ R^{Ipo} |

AntisymmetricObjectProperty(R) | ( x , y ) ∈ R implies ^{Ipo}( y , x ) is not in R^{Ipo} |

TransitiveObjectProperty(R) | R^{Ipo} o R^{Ipo} ⊆ R^{Ipo} |

SubDataPropertyOf(U V) | U ⊆ ^{Ipd}V^{Ipd} |

EquivalentDataProperties(U_{1} ... U_{n}) |
U = _{j}^{Ipd}U for each 1 ≤ _{k}^{Ipd}j , k ≤ n |

DisjointDataProperties(U_{1} ... U_{n}) |
U ∩ _{j}^{Ipd}U is empty for each 1 ≤ _{k}^{Ipd}j , k ≤ n and j ≠ k |

DataPropertyDomain(U C) | { x | ∃ y : (x , y ) ∈ U } ⊆ ^{Ipd}C^{Ic} |

DataPropertyRange(U DR) | { y | ∃ x : (x , y ) ∈ U } ⊆ ^{Ipd}DR^{D} |

FunctionalDataProperty(U) | ( x , y and _{1} ) ∈ U^{Ipd}( x , y imply _{2} ) ∈ U^{Ipd}y_{1} = y_{2} |

SameIndividual(a_{1} ... a_{n}) |
a = _{j}^{Ii}a for each 1 ≤ _{k}^{Ii}j , k ≤ n |

DifferentIndividuals(a_{1} ... a_{n}) |
a ≠ _{j}^{Ii}a for each 1 ≤ _{k}^{Ii}j , k ≤ n and j ≠ k |

ClassAssertion(a C) | a ∈ ^{Ii}C^{Ic} |

ObjectPropertyAssertion(R a b) | ( a ∈ ^{Ii} , b^{Ii} )R^{Ipo} |

NegativeObjectPropertyAssertion(R a b) | ( a is not in ^{Ii} , b^{Ii} )R^{Ipo} |

DataPropertyAssertion(U a v) | ( a ∈ ^{Ii} , v^{D} )U^{Ipd} |

NegativeDataPropertyAssertion(U a v) | ( a is not in ^{Ii} , v^{D} )U^{Ipd} |

Let *O* be an OWL 1.1 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.1 Specification]);
such *I* is then called a *model* of *O*.
A class *C* is satisfiable w.r.t. *O* if there is a model *I* of
*O* such that *C ^{Ic}* is not empty.

- [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.
- [Metamodeling]
- On the Properties of Metamodeling in OWL. Boris Motik. In Proceedings of ISWC-2005
- [OWL 1.1 Specification]
- OWL 1.1 Web Ontology Language: Structural Specification and Functional-Style Syntax. Peter F. Patel-Schneider, Ian Horrocks, and Boris Motik, eds., 2006.
- [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.
- [XML Schema Datatypes]
- XML Schema Part 2: Datatypes Second Edition. Paul V. Biron and Ashok Malhotra, eds. W3C Recommendation 28 October 2004.