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.
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.