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

.

KnowledgeWorks and Prolog User Guide - 4 Apr 2005