
## 5. Properties Of Tabled **Slg(**O)-Resolution

We now present several properties of SLG(O)**-resolution. The first property we** can ensure is that our extension of SLG resolution terminates for the evaluation of any query, generating a final forest. Theorem 5.1 Let q = L **be a query to a doubled Hybrid MKNF knowledge base**
Kd. Then any SLG(O) evaluation of K dfor q **terminates after finitely many steps,**
producing a finite **final forest**.

Proof. **The proof is straightforward since we know already that SLG, i.e.,**
SLG(O) without Oracle Resolution and the extended New Subgoal **operation, terminates finitely for programs with bounded term-depth, and transfinitely**
otherwise (cf. Theorem 5.10 of [Chen and Warren 1996]). Since Definition 2.2 ensures that Hybrid MKNF knowledge bases do not contain recursive terms, i.e.,
non-nullary functors, they have bounded term depth, and so does the doubled knowledge base Kd**. Accordingly, we only have to ensure that the new operation**
Oracle Resolution and the extension of New Subgoal **do not invalidate finite**
termination.

The operation Oracle Resolution **can be applied in the same situation as**
Program Clause Resolution**, namely when creating a new child for a root of**
a tree, so that each operation can be applied only once to a given node (for each of the finitely many rules, respectively for each of the finitely many possible answers of the complete oracle), and this creates one child per successful **application. Now,**
since the knowledge base Kd**is finite, the number of (ground) rule heads is finite.**
Thus, 1) the number of children possibly created with Oracle Resolution for any arbitrary root is finite; and 2) the size of the nodes created is also finite.

The extension of the operation New Subgoal **creates even in the worst case**
finitely many more trees with roots to which only Oracle Resolution **is applicable, which in its turn is fintely many, as just demonstrated.**
We conclude that termination holds for **SLG(**O).

As SLG(O) is defined, there is no prescribed order in which to apply the operations possible in a forest Fi**. For SLG some orders of application are in general**
more efficient than others but, as shown in [Chen and Warren 1996], any order yields the same outcome for any query. This same sort of confluence also holds for SLG(O):
Theorem 5.2 Let E1 and E2 be two SLG(O) evaluations of a query q = L **to a**
doubled Hybrid MKNF knowledge base Kd, F1 the final forest of E1, and F2 the final forest of E2**. Then,** IF1 = IF2.

Proof. **This is a well-known property for SLG as defined using the operations**
of Definition 4.5 excluding the extension of New Subgoal **to classical negation,**
and the operations of Definitions 4.7 and 4.14 (cf. Theorem 5.7 of [Chen and Warren 1996]). Accordingly, we consider cases in which E1 and E2 **make use of the**
operations that have been introduced/extended in SLG(O). However, **Program**
Clause Resolution **is used in SLG, and if we just consider the created children,**
ACM Transactions on Computational Logic, Vol. V, No. N, September 2018.