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) - 22 Dec 2009