# Understanding SLDNF-forest

I am trying to understand this program and the respective forest. This is from the book Logic,Programming and Prolog by Ulf Nilsson.

Question:

• In the main tree, why from ←off_gound(a) can you derive ⧠ ?

• In the main tree, why was chosed on(b,a) first instead of on(c,b)?

Could someone please explain this?

Thank you so much in advance.

• Can you give more details on your second question? I don't see where on(b,a) is chosen in the main tree. I'm assuming the main tree is the big one on the left hand side of the figure? – SimonJ Sep 25 '18 at 6:19
• @SimonJ Yes, the main tree is the big one on the left hand side of the figure. on(b,a) is choosen right after the branch splits to be now two branch – Lw. K Sep 25 '18 at 12:10

## 1 Answer

To answer your first question: SLDNF resolution employs negation as failure to deal with negation.

So from ←$$\neg$$off_ground(a) we derive ⧠ by trying to derive ←off_ground(a) and failing (i.e. deriving FF). This is done in the upper tree on the right hand side.

• Will it always be that way right?, I mean if you have FF in a subtree then in the main tree should be ⧠ ? – Lw. K Sep 25 '18 at 18:27