
Chapter
4:
Declarative Semantics of Logic Programs 187
(i) If a predicate ρ occurs in P. then its definition is contained within
(ii) If a predicate ρ occurs in P
(
under —ι then its definition is contained
within \J
j<i
P
r
(The definition of ρ is the subset of Ρ consisting of all clauses containing ρ on
the left.) A program has a stratification iff it is stratified (Apt, Blair, and
Walker [1988], Lemma 1).
Consider now a stratification (19) of a program P. For every i = Ι,.,.,η, let
T
i
be the operator on Herbrand models (i.e., on sets of ground atoms) defined
as follows: for every Herbrand model M and every ground atom A, A Ε TfM)
iff Α Ε M or ...