




 
The backward chaining inference engine is started to look for any set of bindings which satisfy goal-to-prove . Using those bindings, pattern-to-instantiate is instantiated and returned.
Two values are returned. The second value indicates with 
t 
that a proof was found, or with 
nil
 that no proof exists. In the former case, the first value is the instantiated version of 
pattern-to-instantiate
, in the latter case, the first value is 
nil
.
Any subgoals that match the object base will only find objects from the current inferencing state.
KnowledgeWorks and Prolog User Guide (Windows version) - 6 Dec 2011