Backward chaining involves trying to prove a given goal by using
rules to generate sub-goals and recursively trying to satisfy
those. The KnowledgeWorks backward chaining engine is an
extension of the LispWorks Common Prolog system which can match
directly over KnowledgeWorks CLOS objects (the object base). All
the standard Common Prolog facilities and built in predicates
are available. For more detailed information the reader is
referred to the Common Prolog. Note that all the different ways
of proving a particular goal are defined together in the same
form. KnowledgeWorks and Prolog User Guide (Windows version) - 6
Dec 2011