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.
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.
Atom | Condition 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.