Backward inferencing--the type of inferencing initiated by an ASK operation--can be regarded as a search through a tree of nodes, where each node represents a CycL formula for which bindings are sought, and each link represents a transformation achieved by employing an assertion in the knowledge base.
For example, let's say I ask for bindings for the formula (likesObject ?x ?y). That formula will constitute the root node of an inference search tree. What I am looking for is any assertion which will help provide bindings for ?x and ?y. The KB may contain some ground assertions involving likesObject, such as
(likesObject Keith BillM)
and also some if-then rules, such as
(implies (possesses ?x ?y) (likesObject ?x ?y))
Each of these provides a way to expand the root node. That is, each constitutes a link to a new node with a different formula to satisfy; these new nodes will be the leaf nodes of the search. In the first case, the formula to satisfy in the new node is simply
In the second case, using the if-then rule takes us to a new node that now needs to satisfy the formula
(possesses ?x ?y)
The search procedure may now recurse on this new node, because if we can find bindings for this formula, the if-then rule will give us bindings for our original formula. Perhaps the KB also contains a rule which says,
(implies (objectFoundInLocation ?x KeithsHouse) (possesses Keith ?x))
This assertion can take us to yet another node with the goal formula
(objectFoundInLocation ?x KeithsHouse)
That is, we are now looking for things found in Keith's house, because if something is found in Keith's house, then Keith possesses it, and if someone possesses something, then he or she likes it. Note that this new node has one less free variable than its parent, which is probably desirable.
Alternatively, there may be another rule which states
(implies (and (isa ?x Agent) (owns ?x ?y)) (possesses ?x ?y))
This rule could take us to a new node whose formula to satisfy is
(and (isa ?x Agent) (owns ?x ?y))
But this is probably not a happy development: we are now three nodes down, and the problem is getting more complex, rather than simpler.
Thus, the primary issue to be addressed in designing an inference procedure is the algorithm to be used for searching the tree. How do we decide which leaf nodes to expand next? Another important issue is to determine how a node is expanded. That is, how do we find the axioms in the knowledge base which are likely to provide links to new leaf nodes?