
156 Van
Gelder
• In each remaining rule in RR
k + p
delete all positive subgoals that appear
in
SS
k+
j and delete all negative subgoals that appear in FS
k + x
; these
subgoals are considered proved and the rules "shrink" accordingly.
This completes the description of the transformation Φ(55^, FS
k
, RR
k
).
Figure 2 illustrates the operation of Φ.
For each limit ordinal a, we define
55
a
= U SS„ FS
a
= U FS, RR
a
= Π RR*.
β < a β < a ß<a
Let Ω be the least nonconstructive ordinal, and define
55 = (J 55
ß
FS = U FSp.
β < Ω β < Ω
Also,
we say an atom in the Herbrand universe is unclassified if it is in neither
55 nor FS.
DEFINITION 5
The rule-based negation-as-failure ...