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.