




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 (Macintosh version) - 26 Feb 2015