Database Reference
In-Depth Information
Figure 1. A 2-complete and clash-free completion forest
of
.
Models of Completion Forests
We now show that every model of a KB is preserved in some complete and clash-free completion
tree . If we view all the nodes (either root nodes or generated nodes) in a completion forest as
individual names, we can define models of in terms of models of over an extended vocabulary.
Definition 8.
(Models of completion forests) An interpretation is a model of a completion forest
for , denoted I F , if I K and for all abstract nodes
o
,
¢
and concrete nodes
v
in it holds
that (
i
)
C o
′
≥
(
(
) ³ if 〈 ≥ 〉 ∈
n
C
,
,
n
( , (
ii
)
d
o
v
) ³ if 〈 ≥ 〉 ∈
n
d
,
,
n
( , (
iii
)
R o o
v
(
,
n
′
〉
′
〉
if there exists an abstract edge 〈
o o
, in and 〈 ≥ 〉 ∈ 〈
R
,
,
n
(
o o
,
)
, (
iv
)
T o v
(
,
) ³ if there
n
≠
′
if
o
≠
′
∈ .
exists a concrete edge 〈
o v
, in and 〈 ≥ 〉 ∈ 〈
〉
T
,
,
n
(
o v
,
〉
)
, (
v
)
o
o
We first show that the models of the initial completion forest
F
K
and of coincide.
Lemma 1.
I F
K
iff I K.
Proof.
The only if direction follows from Definition 8. For the if direction, we need to show that, for
all nodes
v
, in
F
K
, Property (
i
)-(
v
) in Definition 8 hold. By Definition 3, each node in
F
K
corre-
sponds to an individual name in . For each abstract individual
o
in
I
, the label of node
o
in
F
K
is
L
(
( ) = {
o
〈 ≥ 〉
C
,
,
n C o
|
( )
≥ ∈
n
A
}
. Since I K, then we have
C o
) ³ and Property (i) thus
n
holds. Property (
ii
)-(
v
) can be proved in a similar way with (
i
).
We then show that, each time an expansion rule is applied, all models are preserved in some result-
ing forest.
Lemma 2.
Let be a completion forest in
,
r
a rule in Table 1,
F
a set of completion forests
obtained from by applying
r
, then for each model of , there exist an ' in
F
and an extension
' of , such that
¢ ¢
I F .
( and I F , then there exists some
o
∈ ∆
, such that
Proof.
∃
≥
-rule. Since 〈∃
R C
.
,
≥ 〉 ∈
,
n
x
( ) ³ hold. In the completion forest obtained from by applying ∃
≥
-rule,
R x o
(
,
) ³ and
C o
n
n
