OWL Rules
Section 3. Direct Model-Theoretic Semantics

Authors:
Peter F. Patel-Schneider, Bell Labs Research, Lucent Technologies
Ian Horrocks, Department of Computer Science, University of Manchester

Contents


3. Direct Model-Theoretic Semantics

The model-theoretic semantics for OWL rules is a straightforward extension of the semantics for OWL given in [OWL S&AS]. The basic idea is that we define bindings, extensions of OWL interpretations that also map variables to elements of the domain. A rule is satisfied by an interpretation iff every binding that satisfies the antecedent also satisfies the consequent. The semantic conditions relating to axioms and ontologies are unchanged, e.g., an interpretation satisfies an ontology iff it satisfies every axiom (including rules) and fact in the ontology.

3.1. Interpreting Rules

Given an abstract OWL interpretation I, a binding B(I) is an abstract OWL interpretation that extends I such that function S maps i-variables to elements of R and d-variables to elements of LVT respectively.

We recall that an Abstract OWL interpretation is a tuple of the form: I = <R, V, EC, ER, S> [OWL S&AS]. An atom is satisfied by an interpretation I under the conditions given in Interpretation Conditions Table.


Interpretation Conditions Table
AtomCondition on Interpretation
description(x) S(x) ∈ EC(description)
property(x,y) <S(x),S(y)> ∈ ER(property)
sameAs(x,y) S(x) = S(y)
differentFrom(x,y) S(x) ≠ S(y)

A binding B(I) satisfies an antecedent A iff A is empty or B(I) satisfies every atom in A. A binding B(I) satisfies a consequent C iff C is not empty and B(I) satisfies every atom in C. A rule is satisfied by an interpretation I iff for every binding B such that B(I) satisfies the antecedent, B(I) also satisfies the consequent.

The semantic conditions relating to axioms and ontologies are unchanged. In particular, an interpretation satisfies an ontology iff it satisfies every axiom (including rules) and fact in the ontology; an ontology is consistent iff it is satisfied by at least one interpretation; an ontology O2 is entailed by an ontology O1 iff every interpretation that satisfies O1 also satisfies O2.