It is straightforward to see that the transformation from the TBox T **to the completed TBox** T
′simply allows us to disregard the mappings S and T **obtained by the**
algorithm of subsumption without losing any of the subset relationships contained in these mappings.

Now we have to show that a reduced TBox, which in general does not **preserve**
EL+ **semantics, is still suitable for the query answering we are interested in, which**
restricts itself to queries of the form C(a) or R(**a, b**).

Proposition 6.4 Let A be an EL+ ABox, T be a completed EL+ **TBox, and** T
′
the reduced EL+ TBox obtained from T **. Then the following two conditions hold.**
(i) a is an instance of concept C in A w.r.t. T iff a **is an instance of concept** C in A **w.r.t.** T
′.

(ii) (a, b) is an instance of role R in A w.r.t. T iff (a, b) **is an instance of role** R
in A **w.r.t.** T
′.

Proof. **For (i) we have to show that** a I ∈ C
I**for every common model** I of A and T iff a I ∈ C
Ifor every common model I of A and T
′**; for (ii) we have to**
show that (a I, bI) ∈ RIfor every common model I of A and T **iff (**a I, bI) ∈ RI
for every common model I of A and T
′**. We are going to sketch the argument for**
(i); the case of (ii) follows analogously.

′ ⇐′**: follows directly from monotonicity: adding GCIs of the form (4) will not**
invalidate any drawn conclusions, i.e. if a I ∈ C
I**for every common model** I of A
and T
′**then adding GCIs of the form (4) can only reduce the common models** of I of A **and never increase. We conclude** a I ∈ C
I**for every common model** I of A
and T .

′ ⇒′**: suppose that** a I ∈ C
Ifor every common model I of A and T **. If none of the**
GCIs of the form (4) contains the concept name C **then we can remove them all** and a I ∈ C
Ifor every common model I of A and T
′**. The same argument applies**
if C appears only on the left hand side of such GCIs. So assume C **appears on the**
right hand side of at least one such GCI C1 ⊑ ∃R.C**. However, even if there is an**
individual i **such that** i I ∈ C
I
1 and (i I, aI) ∈ RI**for every common model** I of A
then T **does not allow to conclude** a I ∈ C
Ifor every common model I of A and T .

We can thus conclude that a I ∈ C
Ifor every common model I of A and T
′.

Having proven that TBox completion does not alter the derivability of **instance**
queries, we can take a short cut: instead of completing the TBox we **can directly** remove all GCIs of the form (4) and discard the mapping T **. We then complete the** TBox only with respect to the mapping S **and obtain the reduced TBox.**
Corollary 6.5 Let T be a EL+ TBox and S and T **be the mappings obtained from**
the subsumption algorithm. We obtain the reduced TBox T
′from T **by removing**
all GCIs of the form (4) from T and by adding for each D ∈ S(C) **a GCI** C ⊑ D.

## 6.3 Transformation Into Rules

Now, we show how to transform the reduced EL+ **KB into rules in such a way that**
running the SLG procedure on the obtained set of rules yields an oracle that can be used in SLG(O)**. Special care must be taken with inconsistencies and with the**
ACM Transactions on Computational Logic, Vol. V, No. N, September 2018.