
## 4.3 Properties Of Reasoning Algorithms

In this section, the main properties of the proposed reasoning algorithms are described.

Theorem 5. The proposed updating and closure processes (Sections 4.1 and 4.2) guarantee a consistent TCN if they are applied on a previous minimal (and consistent) TCN.

Proof: The updating constraint lc'ij is asserted in the TCN if it is consistent with the previous minimal constraint lcij (Consistency-Test function).◊
Theorem 6. The proposed closure algorithm obtains a path-consistent TCN, if it is applied over a previous minimal TCN.

Proof: This was detailed by Barber (1993) for non-disjunctive TCNs and it is applied here to labeled TCNs. We have:
i) No derived constraint can exist between a pair of nodes if no path between them combines the asserted constraint lcij.

ii) The closure process computes a derived constraint between any pair of nodes (nl, nk) that become connected by a path across the closured constraint lcij. Let's assume an existing path between the nodes nx1, ny1 that includes lcij:
nx1, nx2, nx3, ........, nx, (nj lcij nj), ny......, ny2, ny1 such that a derived constraint between nx1 ny1 should be computed. However, a minimal constraint between (nx1, ni) and between (nj, ny1) should already exist in the previous minimal TCN. In consequence, a derived constraint between (nx1, ny1) is computed in the third loop of the process.

iii) If the previous TCN is minimal, all possible derived constraints that can exist between any pair of nodes (nl, nk) are already computed in the constraint lc'lk derived between these nodes in the proposed closure process. In the third loop, this process obtains:
lc'lk= lclk ⊕lc (lcli ⊗lc lcij ⊗lc lcjk).

Let's suppose there exists another path between (nl, nk) across the updated lcij constraint: (nl, np, ni, nj, nq, nk). This path computes another derived constraint between (nl, nk):
lc''lk= lclk ⊕lc (lclp ⊗lc lcpi ⊗lc lcij ⊗lc lcjq ⊗lc lcqk).

However, since the previous TCN is minimal, the previously existing minimal constraints lcli and lcjk imply (lclp ⊗lc lcpi) and (lcjq ⊗lc lcqk), respectively. That is, lcli ⊆lc(lclp ⊗lc lcpi) and lcjk ⊆lc(lcjq ⊗lc lcqk) Thus, lc''lk is also implicitly implied by lc'lk (lc'lk⊆lclc''lk). Here, we have assumed the associative property for ⊗lc, which is obvious from its definition.

iv) Derived constraints obtained in the closure process do not need to be closured again if the previous TCN is minimal. That is, no constraint in the TCN would become more restricted if derived constraints were also closured. Let suppose lclk is modified in the third loop of closure process:
lc'lk= lclk ⊕lc (lcli ⊗lc lcij ⊗lc lcjk)
such that it should be propagated to the (nl, nk, np) subTCN (Figure 8). Thus, the following derived constraints should be obtained: