Show description

The next couple of results are easy consequences of the above lemmas: Lemma 12. Let Π ∈ {L, R}∗, β ∈ {0, 1}∗, q ∈ Q , ut ∈ U. Then Πq ↔∗ST h ut β if and only if there exist b ∈ {0, 1}, q ∈ Q , β ∈ {0, 1}∗ and a rule −−→ ut b → q in ST h such that: (i) β = bβ , and (ii) Πq ↔∗SM q β Proof. The “if” part follows from Lemma 11, thanks to conditions (i) and (ii). For the “only if” part, the assumption implies the existence of b ∈ {0, 1}, such −−→ that β = bβ . By the construction of ST h , there exists a state q and a rule ut b → q ; it is not hard then to show that Πq ↔∗SM q β .

Borgwardt, and B. Morawska (III) Translation of the relevant properties of >. 1) Transitivity and irreflexivity of > is expressed by the clauses [X > X] → and [X > Y ] ∧ [Y > Z] → [X > Z] for all X, Y, Z ∈ Nv . Y ∈ Attr , and i ∈ {0, . . , |T |}. It is easy to see that the set C(Γ, O) can be constructed in time polynomial in the size of Γ and O. In particular, subsumptions B O D between ground atoms B, D can be checked in polynomial time in the size of O [4]. t. the empty ontology. , they stand for non-subsumption rather than subsumption.

R2 . . C will sometimes also be written as ∃r1 r2 . . C, where r1 r2 . . , an element of NR∗ . The role hierarchy induced by O is a binary relation O on NR , which is defined as the reflexive-transitive closure of the relation {(r, s) | r s ∈ O}. Using elementary reachability algorithms, the role hierarchy can be computed in polynomial time in the size of O. It is easy to see that r O s implies that rI ⊆ sI for all models I of O. 34 3 F. Baader, S. Borgwardt, and B. Morawska Unification In order to define unification, we first introduce the notion of a substitution operating on concept descriptions.