where S is the underlying subgoal of G. Assume Fn **contains no tree with root**
S. Then add the tree S ← |S to Fn.

(2) Program Clause Resolution: Let Fn **contain a tree with root node** N =
S ← |S and C be a rule Head ← Body such that Head unifies with S **with**
mgu θ. Assume that in Fn, N does not have a child Nchild = (S ← |**Body**)θ.

Then add Nchild **as a child of** N.

(3) Positive Return: Let Fn contain a tree with non-root node N **whose selected**
literal S is positive. Let Ans be an answer for S in Fn and Nchild **be the** SLG(O) resolvent of N and Ans on S. Assume that in Fn, N **does not have** a child Nchild. Then add Nchild **as a child of** N.

As illustrated in Example 4.1, the operation New Subgoal **creates a new tree**
in the forest F for a selected literal in the Goals **of some (non-root) node in a tree**
in F. Once a root node N for a positive literal is created, the **Program Clause** Resolution operation can create children for N**, given the rules in the knowledge**
base. Positive Return **resolves positive literals in nodes, with answers already** in the forest, according to Definition 4.3. Contrary to SLG, the **New Subgoal**
operation may also create new trees for classically negated literals to which only the operation Oracle Resolution**, defined below, applies.**
Now, if a sequence of SLG(O) **operations yields a (possibly intermediate) forest**
containing an unconditional answer, then this answer is considered **to be true.** Likewise, if no more operations are applicable to a set of trees, and none of them contains an unconditional answer, i.e., the set of literals associated **to these trees is** completely evaluated (see Definition 4.12), then we can interpret all **these literals as** false. Expanding on this correspondence, we may associate an SLG(O) **forest with** a partial interpretation, taking into consideration that, besides atoms and default negated atoms, SLG(O) **also allows classically negated literals as the roots of trees.**
This interpretation is shown to correspond to MW F **(cf. Theorem 5.3 below).**
Definition 4.6 Let F be a forest. Then the interpretation induced by F, IF **, is**
the smallest set such that:
—A (ground) atom A ∈ IF iff A **is in the ground instantiation of some unconditional**
answer Ans ← | in F.

—A (ground) negated atom ¬A ∈ IF iff ¬A **is in the ground instantiation of some**
unconditional answer Ans ← | in F.

—A (ground) literal not A ∈ IF iff A **is in the ground instantiation of a literal**
whose tree in F is marked as complete, and A **is not in the ground instantiation** of any answer in a tree in F.

An atom S is successful (resp. failed**) in** F if S
′(resp. not S
′) is in IF **for every**
S
′**in the ground instantiation of** S.

Whenever an atom A is successful, we can fail its default negation not A**. If an**
atom A is failed, then we can simplify away not A**. Ground default negated literals** that are neither failed nor successful may be delayed and be simplified later. More precisely:
ACM Transactions on Computational Logic, Vol. V, No. N, September 2018.