###
3.2.5 The Backward Chaining Interpreter

The backward chaining interpreter can be invoked from Lisp by the following functions

```
(any <expr-to-instantiate> <expr-to-prove>)
```

which finds any solution to ```
<expr-to-prove>
```

and instantiates ```
<expr-to-instantiate>
```

, and

```
(findall <expr-to-instantiate> <expr-to-prove>)
```

finds all the solutions to ```
<expr-to-prove>
```

, instantiates ```
<expr-to-instantiate>
```

for each and returns these in a list.

For other interface functions to be called from Lisp the reader is referred to Common Prolog.

From the action part of a forward chaining rule the backward chainer is called implicitly when a CLOS match or goal expression is used. The action part of forward chaining rules and the antecedents of backward chaining rules are syntactically and semantically identical.

*KnowledgeWorks and Prolog User Guide (Unix version) - 6 Dec 2011*