###
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 - 4 Apr 2005