Direct Semantics

Authors

Bernardo Cuenca Grau, Oxford University

Boris Motik, Oxford University

Contributors

Ian Horrocks, Oxford University

Bijan Parsia, The University of Manchester

Peter F. Patel-Schneider, Bell Labs Research, Alcatel-Lucent

Ulrike Sattler, The University of Manchester

1 Introduction

This document defines the formal semantics of OWL 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 [SROIQ]. Unfortunately, the definition of SROIQ does not provide for datatypes and punning. Therefore, the semantics of OWL 2 is defined in a direct model-theoretic way, by interpreting the constructs of the functional-style syntax from [OWL 2 Specification]. 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 formal semantics for OWL Lite and OWL DL and is equivalent to the official definition [OWL Abstract Syntax and Semantics].

OWL 2 allows for annotations of ontologies and ontology entities (classes, properties, and individuals) and ontology axioms. Annotations, however, have no semantic meaning in OWL 2 and are ignored in this document.

OWL 2 declarations are not interpreted directly; they are simply used 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 the tables in this document.

2 Model-Theoretic Semantics for OWL 2

This section specifies the model-theoretic semantics of OWL 2 ontologies in the functional-style syntax.

2.1 Datatype Maps

A datatype map is a 4-tuple D = ( N_DT , N_LT , ⋅ ^DT , ⋅ ^LT ) that defines the set of supported datatypes and their interpretation.

• N_DT is a set of datatypes as defined in the OWL 2 Specification [OWL 2 Specification], each associated with a positive integer arity, containing at least the unary datatype rdfs:Literal.
• N_LT is a function that assigns to each datatype DT ∈ N_DT a set of literals N_LT(DT); this set is sometimes also called a lexical space of DT; furthermore, N_LT(rdfs:Literal) = ∅. The set of all literals for all datatypes is given as the set N_LT (whether N_LT is used as a function or as a set of all literals is expected to be clear from the context).
• For each n-ary datatype DT ∈ N_DT \ { rdfs:Literal }, the function ⋅ ^DT assigns to DT an n-ary relation (DT)^DT called a value space.
• For each unary datatype DT ∈ N_DT \ { rdfs:Literal } and each literal lt ∈ N_LT(DT), the function ⋅ ^LT assigns to lt a data value (lt)^LT ∈ (DT)^DT.

The value spaces of the XML Schema Datatypes and the mappings of their literals to data values is defined as in XML Schema Datatypes [XML Schema Datatypes]. The value space for owl:internationalizedString consists of all pairs <"text",languageTag>, where "text" is a string and languageTag is a language tag.

2.2 Vocabulary

Given a datatype map D = ( N_DT , N_LT , ⋅ ^DT , ⋅ ^LT ), a vocabulary (or signature) V = ( N_C , N_OP , N_DP , N_I , N_DT , N_LT ) over D is a 6-tuple consisting of the following elements:

• N_C is a set of classes as defined in OWL 2 Specification [OWL 2 Specification], containing at least the classes owl:Thing and owl:Nothing.
• N_OP is a set of object properties as defined in OWL 2 Specification [OWL 2 Specification].
• N_DP is a set of data properties as defined in OWL 2 Specification [OWL 2 Specification].
• N_I is a set of individuals as defined in OWL 2 Specification [OWL 2 Specification].
• N_DT is the set of all datatypes of D.
• N_LT is a set of all literals of D.

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 data type;
• DR denotes a data range;
• a denotes an individual; and
• lt denotes a literal.

2.3 Interpretations

Given a datatype map D and a vocabulary V over D, an interpretation Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT ) is a 8-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, for each datatype DT ∈ N_DT and each tuple < α₁ , ... , α_k > ∈ (DT)^DT, it is the case that α_i ∈ Δ_D for each 1 ≤ i ≤ k.
• ⋅ ^C is the class interpretation function that assigns to each class C ∈ N_C \ { owl:Thing , owl:Nothing } a subset C^C ⊆ Δ_Int.
• ⋅ ^OP is the object property interpretation function that assigns to each object property OP ∈ N_OP \ { owl:TopObjectProperty , owl:BottomObjectProperty } a subset (OP)^OP ⊆ Δ_Int × Δ_Int.
• ⋅ ^DP is the data property interpretation function that assigns to each data property DP ∈ N_DP \ { owl:TopDataProperty , owl:BottomDataProperty } a subset (DP)^DP ⊆ Δ_Int × Δ_D.
• ⋅ ^I is the individual interpretation function that assigns to each individual a ∈ N_I an element a^I ∈ Δ_Int.
• ⋅ ^DT and ⋅ ^LT are the same as in D.

The following sections define the extensions of ⋅ ^OP , ⋅ ^DT , and ⋅ ^C to object property expressions, data ranges, and class expressions. Since data property expressions are currently restricted to data properties, it is not necessary to define an extension of ⋅ ^DP to data property expressions.

2.3.1 Object Property Expressions

The object property interpretation function ⋅ ^OP is extended to object property expressions as shown in Table 1.

2.3.2 Data Property Expressions

The data property interpretation function ⋅ ^DP is extended to data property expressions as shown in Table 2.

2.3.3 Data Range Expressions

The datatype interpretation function ⋅ ^DT is extended to data ranges as shown in Table 3.

2.3.4 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.

2.4 Models

An interpretation Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT ) is called a model of an axiom w.r.t. ontology O if the axiom is satisfied in Int according to the following definitions. The function ISNAMED is defined for each α ∈ Δ_Int such that ISNAMED(α) = true if and only if an individual a exists such that it occurs in the axiom closure of O and a^I = α.

2.4.1 Class Expression Axioms

Satisfaction of OWL 2 class expression axioms in Int w.r.t. O is defined as shown in Table 5.

2.4.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.

2.4.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.

2.4.4 Object and Data Property Expression Axioms

Satisfaction of OWL 2 axioms about both object and data property expressions in Int w.r.t. O is defined as shown in Table 8.

2.4.5 Assertions

Satisfaction of OWL 2 assertions in Int w.r.t. O is defined as shown in Table 9.

2.4.6 Ontologies

Int is a model of an OWL 2 ontology O if it is a model w.r.t. O for each the axioms in the axiom closure of O. (Note that anonymous individuals must be properly renamed apart, as described in Section 4.6.2 of the OWL 2 Specification [OWL 2 Specification].)

2.5 Inference Problems

Let O and O' be OWL 2 ontologies, CE, CE₁, and CE₂ class expressions, and a a named individual.

• O is satisfiable (or consistent) if a model of O exists.
• O entails O' if every model of O is also a model of O'.
• O and O' are equivalent if O entails O' and O' entails O.
• O and O' are equisatisfiable if O is satisfiable if and only if O' is satisfiable.
• CE is satisfiable w.r.t. O if a model Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT ) of O exists such that (CE)^C ≠ ∅.
• CE₁ is a subclass of CE₂ w.r.t. O if (CE₁)^C ⊆ (CE₂)^C for each model Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT ) of O.
• a is an instance of CE w.r.t. O if a^I ∈ C^CE for each model Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT ) of O.

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 is made precise by the following theorem.

Theorem 1. Let O₁ and O₂ be OWL 2 ontologies, D = ( N_DT , N_LT , ⋅ ^DT , ⋅ ^LT ) a datatype map such that each datatype mentioned in O₁ and O₂ occurs in N_DT, and D' = ( N_DT' , N_LT' , ⋅ ^DT' , ⋅ ^LT' ) a datatype map such that N_DT ⊆ N_DT', N_LT ⊆ N_LT', and ⋅ ^DT' and ⋅ ^LT' are extensions of ⋅ ^DT and ⋅ ^LT. Then, O₁ entails O₂ w.r.t. D if an only if O₁ entails O₂ w.r.t. D'.

Proof. The theorem is proved by showing the contrapositive: an interpretation Int w.r.t. D exists such that O₁ is and O₂ is not satisfied in Int if and only if an interpretation Int' w.r.t. D' exists such that O₁ is and O₂ is not satisfied in Int'. The (⇐) direction is trivial since each interpretation Int w.r.t. D' is also an interpretation w.r.t. D. For the (⇒) direction, assume that an interpretation Int = ( Δ_Int , Δ_D , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT ) w.r.t. D exists such that O₁ is and O₂ is not satisfied in Int. Let Int' = ( Δ_Int , Δ_D' , ⋅ ^C , ⋅ ^OP , ⋅ ^DP , ⋅ ^I , ⋅ ^DT , ⋅ ^LT ) be an interpretation where all the components are the same as in Int apart from Δ_D', which is defined obtained by extending Δ_D with the value space of all datatypes in N_DT' \ N_DT. Clearly, ComplementOf( DT )^DT ⊆ ComplementOf( DT )^DT' for each datatype DT ∈ N_DT. The interpretation of data properties is the same in Δ_Int and Δ_Int', so (CE)^CE = (CE)^CE' for each class expression CE occurring in O₁ and O₂. Therefore, O₁ is and O₂ is not satisfied in Int'. QED

This theorem allows OWL 2 implementations to interpret each OWL 2 ontology O by considering only the datatypes explicitly occurring in O. Furthermore, it shows that tools can support datatypes not explicitly mentioned in this specification without fear that this will change the semantics of OWL 2 ontologies that do not use these datatypes.

4 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. 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.

[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).