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.