
Chapter
2:
Towards
a
Theory
of
Declarative Knowledge
129
previous step
iff (by clause (3) of Definition 18)
I
p
(
-\B, -iB,S U S
T
_,β) for every negative leaf
-iB of Τ
iff (by rules (1) and (2) of 18)
7
p
(root(T),T,S).
(2)
"
We now give the theorem that, in effect, says the interpreter unambiguously
"computes" the standard model M
p
of P, when Ρ is stratified. The statement
of the theorem may at first seem a bit arcane, but recall that the definition of I
p
does not in general uniquely determine a relation on Ü x IT x 2
U
. We are
about to show, under the assumption that Ρ is stratified, that if the definition of
I
p
is satisfied on Ü x IT x 2
U
, the ...