Database Reference
In-Depth Information
First, DTD D =( d, r ) is defined as follows.
d ( r )= x,
d ( x )=( E x |x )( x|B c |E x ) ,
d ( B c )= cc,
d ( c )=( T c |F c )( c|E c ) ,
d ( E x )= d ( E x )= d ( E c )= d ( T c )= d ( F c )= .
Note that D is independent of φ since D is fixed. In contrast, D depends on φ
in the proof of Theorem 1 in Ref. [10].
Second, query q is defined as follows.
m
q = /r
/x/
···
/x /E x
(1)
/ ↑
:: x/P m / ↑
:: x/P m− 1 / ↑
:: x/ ···/ ↑
:: x/P 1 / ↑
:: x/ ↑
:: r
(2)
/Q 1 /Q 2 / ···/Q n ,
(3)
where P m ,P m− 1 , ··· ,P 1 in (2) and Q 1 ,Q 2 , ··· ,Q n in (3) are subqueries defined
later. In short, according to φ subqueries (1) and (2) plot a tree t showninFig.1,
and then subquery (3) checks whether φ is satisfiable over t .Eachsubquery P i
plots the “subtree” P i in t , as shown in Fig. 1. Formally, P i is defined as follows
(1
≤ i ≤ m ).
m−i
+1
/x/E x / ↑
:: x/ ···/x/E x / ↑
P i =
:: x/B c
(4)
/c/T i, 1 / ↑
:: c/c/T i, 2 / ↑
:: c/ ···/c/T i,n− 1 / ↑
:: c/c/T i,n / ↑
:: c
(5)
n +1
/ ↑
:: c/ ···/ ↑
:: c/B c
(6)
/c/F i, 1 / ↑
:: c/c/F i, 2 / ↑
:: c/ ···/c/F i,n− 1 / ↑
:: c/c/F i,n / ↑
:: c
(7)
n +1
/ ↑ :: c/ ···/ ↑ :: c/B c
(8)
n +1
/c/ ···/c /T c / ↑
n +1
:: c/E c
/ ↑
:: c/ ···/ ↑
:: c/↑
:: B c
(9)
n +1
/c/ ···/c /F c / ↑
n +1
:: c/E c
/ ↑
:: c/ ···/ ↑
:: c/↑
:: B c
(10)
m−i +1
/ ↑
:: x/ ···/ ↑
:: x.
(11)
Starting from the x -node at position x i in t (Fig. 1), the context node goes down
to B c by (4). Then subquery (5) sets the value of T i,j for 1
≤ j ≤ n and subquery
(7) sets those of F i,j
for 1
≤ j ≤ n ,where
 
Search WWH ::




Custom Search