Backward Chaining

Overview of "Backward-Chaining"

To do backward-chaining, Pyke finds rules whose then part matches the goal (i.e., the question). Once it finds such a rule, it tries to (recursively) prove all of the subgoals in the if part of that rule. Some of these subgoals are matched against facts, and others are subgoals for other backward-chaining rules. If all of the subgoals can be proven, the rule succeeds and the original goal is proven. Otherwise, the rule fails, and Pyke tries to find another rule whose then part matches the goal, and so on.

So Pyke ends up linking (or chaining) the if part of the first rule to the then part of the next rule.

Reviewing:

1. Pyke starts by finding a rule whose then part matches the goal.
2. Pyke then proceeds to process the if part of that rule.
3. Which may link (or chain) to the then part of another rule.

Since Pyke processes these rules from then to if to then to if in the reverse manner that we normally think of using rules, it's called backward chaining.

To make this more clear, Pyke has you write your backward-chaining rules upside down by writing the then part first (since that's how it is processed).

"Use", "When" Rather than "Then", "If"

But then-if rules sound confusing, so Pyke uses the words use and when rather than then and if. You can then read the rule as "use" this statement "when" these other statements can be proven.

Example

Consider this example:

 1  direct_father_son
 2      use father_son($father, $son, ())
 3      when
 4          family2.son_of($son, $father)

 5  grand_father_son
 6      use father_son($grand_father, $grand_son, (grand))
 7      when
 8          father_son($father, $grand_son, ())
 9          father_son($grand_father, $father, ())

10  great_grand_father_son
11      use father_son($gg_father, $gg_son, (great, $prefix1, *$rest_prefixes))
12      when
13          father_son($father, $gg_son, ())
14          father_son($gg_father, $father, ($prefix1, *$rest_prefixes))

15  brothers
16      use brothers($brother1, $brother2)
17      when
18          father_son($father, $brother1, ())
19          father_son($father, $brother2, ())
20          check $brother1 != $brother2

21  uncle_nephew
22      use uncle_nephew($uncle, $nephew, $prefix)
23      when
24          brothers($uncle, $father)
25          father_son($father, $nephew, $prefix1)
26          $prefix = ('great',) * len($prefix1)

27  cousins
28      use cousins($cousin1, $cousin2, $distance, $removed)
29      when
30          uncle_nephew($uncle, $cousin1, $prefix1)
31          father_son($uncle, $cousin2, $prefix2)
32          $distance = min(len($prefixes1), len($prefixes2)) + 1
33          $removed = abs(len($prefixes1) - len($prefixes2))

We can draw something similar to a function call graph with these rules:

Example Rules

These rules are not used until you ask Pyke to prove a goal.

The easiest way to do this is with some_engine.prove_1_goal or some_engine.prove_goal. Prove_1_goal only returns the first proof found and then stops (or raises pyke.knowledge_engine.CanNotProve). Prove_goal returns a context manager for a generator that generates all possible proofs (which, in some cases, might be infinite).

Both functions return the pattern variable variable bindings, along with the plan.

Backtracking with Backward-Chaining Rules

For this example, these are the starting set of family2 facts:

1  son_of(tim, thomas)
2  son_of(fred, thomas)
3  son_of(bruce, thomas)
4  son_of(david, bruce)

And we want to know who fred's nephews are. So we'd ask uncle_nephew(fred, $nephew, $prefix).

Here are the steps (in parenthesis) in the inferencing up until the first failure is encountered (with the line number from the example preceding each line):

(1)   22  use uncle_nephew(fred, $nephew, $prefix)
          24  brothers(fred, $father)
(2)           16  use brothers(fred, $brother2)
                  18  father_son($father, fred, ())
(3)                   2  use father_son($father, fred, ())
                          4  family2.son_of(fred, $father)
                               matches fact 2: son_of(fred, thomas)
                  19  father_son(thomas, $brother2, ())
(4)                   2  use father_son(thomas, $son, ())
                          4  family2.son_of($son, thomas)
                               matches fact 1: son_of(tim, thomas)
                  20  check fred != tim
          25  father_son(tim, $nephew, $prefix1)
(5.1)         2  use father_son(tim, $son, ())
                  4  family2.son_of($son, tim)                               => FAILS
(5.2)         6  use father_son(tim, $grand_son, (grand))
                  8  father_son(tim, $grand_son, ())
                      2  use father_son(tim, $son, ())
                          4  family2.son_of($son, tim)                       => FAILS
(5.3)         11 use father_son(tim, $gg_son, (great, $prefix1, *$rest_prefixes))
                  13 father_son(tim, $gg_son, ())
                      2  use father_son(tim, $son, ())
                          4  family2.son_of($son, tim)                       => FAILS

Each rule invocation is numbered (in parenthesis) as a step number. Step 5 has tried 3 different rules and they have all failed (5.1, 5.2 and 5.3).

If you think of the rules as functions, the situation now looks like this (the step numbers that succeeded circled in black, and steps that failed circled in red):

We Need to Backtrack!

At this point, Pyke has hit a dead end and must backtrack. The way that backtracking proceeds is to go back up the list of steps executed, combining the steps from all rules into one list. Thus, when step 5 fails, Pyke backs up to step 4 and tries to find another solution to that step.

If another solution is found, Pyke proceeds forward again from that point. If no other solutions are found, Pyke backs up another step.

When Pyke goes back to step 4, the next solution binds $son to fred. This fails the subsequent check in the brothers rule:

20          check $brother1 != $brother2

And so Pyke goes back to step 4 once again. The next solution binds $son to bruce. This succeeds for brother and is passed down to father_son which returns david as fred's nephew.

Further backtracking reveals no other solutions.

Running the Example

>>> from pyke import knowledge_engine
>>> engine = knowledge_engine.engine(__file__)
>>> engine.activate('bc_related')

Nothing happens this time when we activate the rule base, because there are no forward-chaining rules here.

We want to ask the question: "Who are Fred's nephews?". This translates into the Pyke statement: bc_related.uncle_nephew(fred, $v1, $v2).

This is 'bc_related', 'uncle_nephew', with ('fred',) followed by 2 pattern variables as arguments:

>>> from __future__ import with_statement
>>> with engine.prove_goal('bc_related.uncle_nephew(fred, $nephew, $distance)') as gen:
...     for vars, no_plan in gen:
...         print vars['nephew'], vars['distance']
david ()