
Chapter 16: Equivalences of Logic Programs 641
PROPOSITION 5
If Ρ is subsumption-equivalent to a program that is locally deterministic and
such that no clause has local variables, then T
p
is down-distributive.
Proof:
By Theorem 3 T
p
is down-continuous. Thus, it suffices to prove that
T
P
(X ΠΥ) = T
P
{X) Π Τ
Ρ
(Υ) VX, Y. Further, by Theorem 2, it suffices to con-
sider only the case where Ρ is locally deterministic and such that no clause has
local variables. Let X, Y QHB. Since T
p
is monotonie, VX, Υ T
P
(X Π Y) C
Tp(X) Π Τρ(Υ). Suppose Α Ε Τ
Ρ
(Χ) Π Τ
Ρ
(Υ). Then, since there is only one in-
stance of a clause of the form A —
B
v
...,B
n
,
we have that {B