The model-theoretic semantics for SWRL is a straightforward extension of the semantics for OWL given in the OWL Semantics and Abstract Syntax document [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.
From the OWL Semantics and Abstract Syntax document we recall that an abstract OWL interpretation is a tuple of the form
I = <R, EC, ER, L, S, LV>
where R is a set of resources, LV ⊆ R is a set of literal values, EC is a mapping from classes and datatypes to subsets of R and LV respectively, ER is a mapping from properties to binary relations on R, L is a mapping from typed literals to elements of LV, and S is a mapping from individual names to elements of EC(owl:Thing).
Given an abstract OWL interpretation Ι, a binding B(Ι) is an abstract OWL interpretation that extends Ι such that S maps i-variables to elements of EC(owl:Thing) and L maps d-variables to elements of LV respectively. An atom is satisfied by an interpretation Ι under the conditions given in the Interpretation Conditions Table, where C is an OWL DL description, P is an OWL DL individualvalued property, Q is an OWL DL datavalued property, x,y are variables or OWL individuals, and z is a variable or an OWL data value.
|Atom||Condition on Interpretation|
|C(x)||S(x) ∈ EC(C)|
|P(x,y)||<S(x),S(y)> ∈ ER(P)|
|Q(x,z)||<S(x),L(z)> ∈ ER(Q)|
|sameAs(x,y)||S(x) = S(y)|
|differentFrom(x,y)||S(x) ≠ S(y)|
A binding B(Ι) satisfies an antecedent A iff A is empty or B(Ι) satisfies every atom in A. A binding B(Ι) satisfies a consequent C iff C is not empty and B(Ι) satisfies every atom in C. A rule is satisfied by an interpretation Ι iff for every binding B such that B(Ι) satisfies the antecedent, B(Ι) 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.