.. Copyright ÂŠ 2007 Bruce Frederiksen
.. Permission is hereby granted, free of charge, to any person obtaining a copy
.. of this software and associated documentation files (the "Software"), to deal
.. in the Software without restriction, including without limitation the rights
.. to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
.. copies of the Software, and to permit persons to whom the Software is
.. furnished to do so, subject to the following conditions:
.. The above copyright notice and this permission notice shall be included in
.. all copies or substantial portions of the Software.
.. THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
.. IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
.. FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
.. AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
.. LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
.. OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
.. THE SOFTWARE.
crumb: Backward Chaining
Explanation of backward-chaining rules.
Backward chaining rules_ are processed when your program asks pyke to prove_
a specific *goal*. Pyke will only use activated_ `rule bases`_ to do the
Consider this example::
2 use child_parent($son, $father, (), son, father)
4 family.son_of($son, $father, $_)
6 use child_parent($son, $mother, (), son, mother)
8 family.son_of($son, $_, $mother)
10 use child_parent($daughter, $father, (), daughter, father)
12 family.daughter_of($daughter, $father, $_)
14 use child_parent($daughter, $mother, (), daughter, mother)
16 family.daughter_of($daughter, $_, $mother)
18 use child_parent($grand_child, $grand_parent, (grand),
19 $grand_child_type, $grand_parent_type)
21 child_parent($grand_child, $parent, (), $grand_child_type, $_)
22 child_parent($parent, $grand_parent, (), $_, $grand_parent_type)
24 use child_parent($gg_child, $gg_parent, (great, $prefix1, *$rest_prefixes),
25 $gg_child_type, $gg_parent_type)
27 child_parent($gg_child, $parent, (), $gg_child_type, $_)
28 child_parent($parent, $gg_parent, ($prefix1, *$rest_prefixes),
29 $_, $gg_parent_type)
Identifying Backward-Chaining Rules
These rules_ draw the same conclusions as the forward-chaining_ example_;
but you'll notice three differences:
#. The `rule's`_ **if** and **then** parts are reversed.
#. The rules_ use different keywords: ``use`` for the **then** clause
and ``when`` for the **if** clause.
#. The facts_ established by backward-chaining do not have a knowledge
base name prefix. In this case, the knowledge base name defaults to
the `rule base category`_ of this `rule base`_ (it's root rule base name).
How Backward-Chaining Rules are Run
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_ or *some_engine*.prove_n_. Prove_1_ only
returns the first proof found and then stops (or raises pyke.CanNotProve).
Prove_n_ is a generator that generates all possible proofs (which, in
some cases, might be infinite). In both cases, you pass a tuple of
arguments and the number of variable arguments as the last two parameters.
The total number of arguments for the goal is the sum of the length of the
actual arguments that you pass plus the number of variable arguments that you
Both functions return the variable bindings for the number of variable
arguments you specified as a tuple, along with the plan_.
Running the Example
>>> import pyke
>>> engine = pyke.engine('examples')
>>> engine.assert_('family', 'son_of', ('michael', 'bruce', 'marilyn'))
>>> engine.assert_('family', 'son_of', ('bruce', 'thomas', 'norma'))
>>> engine.assert_('family', 'daughter_of', ('norma', 'allen', 'ismay'))
>>> for vars, no_plan in engine.prove_n('bc_example', 'child_parent',
... ('michael',), 4):
... print vars
('bruce', (), 'son', 'father')
('marilyn', (), 'son', 'mother')
('thomas', ('grand',), 'son', 'father')
('norma', ('grand',), 'son', 'mother')
('allen', ('great', 'grand'), 'son', 'father')
('ismay', ('great', 'grand'), 'son', 'mother')
Pyke performs the proof by:
#. Checking to see if the goal is simply a known fact_.
If so, it has a proof!
#. Look for the first backward-chaining rule_ that concludes the goal
in its ``use`` clause.
* If not found, the goal fails.
* If found, try to recursively prove all of the subgoals in the
`rule's`_ ``when`` clause.
* If this succeeds, the goal is proven.
* If this fails, go back to step 2 and look for the next rule
that concludes the goal in its ``use`` clause.
Note how the rules_ are combined in the opposite direction from
forward-chaining_ rules_. Here the first `rule's`_ **if** (``when``) clause is
linked backwards to the next rule's **then** (``use``) clause.
This is why these rules are called *backward-chaining* rules. This is also
referred to as *goal directed*, since the inferencing is driven by the final
Also note that while processing each subgoal within a `rule's`_ ``when`` clause:
* If pyke succeeds at proving the subgoal:
* Pyke will proceed to the next subgoal within the ``when`` clause.
* If pyke reaches the end of the ``when`` clause, the rule_ succeeds.
* If pyke fails at proving the subgoal:
* Pyke will back up to the prior subgoal within the ``when`` clause
and try to find another proof for it. The process starts over
from this prior subgoal, going forward or backing up depending on
whether another proof can be found.
* If pyke reaches the beginning of the ``when`` clause, the rule_
Thus, execution within each `rule's`_ ``when`` clause proceeds both forwards
and backwards up and down the list of subgoals, depending on whether each
subgoal succeeds or fails. The process of backing up in the ``when``
clause to try alternate subproofs is called *backtracking*.
.. _activated: ../../using_pyke.html#setting-up-each-case
.. _example: forward_chaining.html#example
.. _fact: ../knowledge_bases/fact_bases.html#facts
.. _facts: fact_
.. _forward-chaining: forward_chaining.html
.. _plan: ../plans.html
.. _prove: ../../using_pyke.html#proving-goals
.. _prove_1: prove_
.. _prove_n: `prove_1`_
.. _pyke.prove_1: `prove_1`_
.. _pyke.prove_n: `prove_n`_
.. _rule: index.html
.. _rule base: ../knowledge_bases/rule_bases.html
.. _rule base category: ../knowledge_bases/rule_bases.html#rule-base-categories
.. _rule bases: `rule base`_
.. _rules: rule_
.. _rule's: rule_