International Journal of Web & Semantic Technology (IJWest) Vol.1, Num.4, October 2010

![0_image_0.png](0_image_0.png)

Function **MakeSets(**v)

1 **Initialize set of variable sets** v ret = {};
2 while v **is not empty** do 3 Find a query q **that instantiates some of the variables in** v; 4 Initialize variable set v**temp** = {};
5 forall the variable ϕi ∈ v and ϕi **is instantiated by** q do 6 v ← v − {ϕi}; 7 vtemp ← vtemp ∪ {ϕi};
8 end 9 v ret ← v ret ∪ {v**temp**};
10 end
Function **GenerateAssignableSet(**q, S
t)
/* Suppose q is made with the concepts C1**, ..., C**n and ϕi1**, . . . , ϕ**ik are the uninstantiated

![0_image_1.png](0_image_1.png)

variables corresponding to the concept Ci */
1 v ← {ϕij | ϕij 6= ∗};
2 if S
t == Φ **then**
/* All the variables of q are uninstantiated */
3 Tuple set T ← (C1 ⋊⋉ C2 ⋊⋉ ... ⋊⋉ Cn);
4 **else**
/* Some of the variables of q are previously instantiated and t1**, ..., t**m ∈ S
tare the tuple sets corresponding to those variables */
5 Tuple set T ← (C1 ⋊⋉ C2 ⋊⋉ . . . ⋊⋉ Cn ⋊⋉ t1 ⋊⋉ **. . .** ⋊⋉ tm);
6 end 7 **Relational algebra query** q Rel ← πv(T );
8 **Compute** q Rel **and return the set of tuples;**
Function SplitAssignableSet(δ, v**split**, c)

![0_image_2.png](0_image_2.png)

/* Suppose c1, · · · , ci ∈ c */
1 **Relational algebra query** q Rel ← σ(c1∨c2∨...∨ci)(δ);
2 **Compute** q Rel **and return the set of tuples;**
This algorithm can also be used by the server as the protocol progresses(described as Scenario-4 in Section 1). In that case, the variables in the queries which are already executed, have some value assigned to them and those variables will be considered as instantiated **by the algorithm.**

## 5.4 Proof Of Correctness

The proof of correctness of Algo. 3 is presented below. Algo. 3 verifies the spuriousness of conflicts returned by Algo. 1 on the server database.

Theorem 3. **[Soundness] Algorithm 3 correctly reports the spuriousness of conflict on the set of variables** v
′
**, where** v
′ = v ∪ RestrictSet(v) and v **is the set of previously instantiated variables in a query**
q of protocol P **with ontological conflict.**
Proof. The proof is done using induction. We do the induction on the integer parameter n**, where** n is the total number of VerifyConflict function calls done by Algorithm 3 for q**. Among the different**
VerifyConflict **function calls, first call is done by Algorithm 3 and the others are recursive calls.**
[Basis (n = 1) :] In this case RestrictSet(v) = φ. In this case if the AssignableSet(v) is ∅ **Algo. 3**
correctly reports the conflict as spurious, otherwise Algo. 3 reports the conflict as not spurious, which is correct.

40