.. $Id: backward_chaining.txt 72 2008-03-06 03:03:50Z mtnyogi $
.. 
.. 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.

restindex
    crumb: Backward Chaining
    page-description:
        Explanation of backward-chaining rules.
    /description
    format: rest
    encoding: utf8
    output-encoding: utf8
    include: yes
    initialheaderlevel: 3
/restindex

=============================================
Backward Chaining
=============================================

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
proof.

Example
=================

Consider this example::

     1  son_father:
     2      use child_parent($son, $father, (), son, father)
     3      when
     4          family.son_of($son, $father, $_)
        
     5  son_mother:
     6      use child_parent($son, $mother, (), son, mother)
     7      when
     8          family.son_of($son, $_, $mother)
        
     9  daughter_father:
    10      use child_parent($daughter, $father, (), daughter, father)
    11      when
    12          family.daughter_of($daughter, $father, $_)
        
    13  daughter_mother:
    14      use child_parent($daughter, $mother, (), daughter, mother)
    15      when
    16          family.daughter_of($daughter, $_, $mother)
        
    17  grand_parent_and_child:
    18      use child_parent($grand_child, $grand_parent, (grand),
    19                       $grand_child_type, $grand_parent_type)
    20      when
    21          child_parent($grand_child, $parent, (), $grand_child_type, $_)
    22          child_parent($parent, $grand_parent, (), $_, $grand_parent_type)
        
    23  great_grand_parent_and_child:
    24      use child_parent($gg_child, $gg_parent, (great, $prefix1, *$rest_prefixes),
    25                       $gg_child_type, $gg_parent_type)
    26      when
    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
specify.

Both functions return the variable bindings for the number of variable
arguments you specified as a tuple, along with the plan_.

Running the Example
========================

    >>> from pyke import knowledge_engine
    >>> engine = knowledge_engine.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'))
    >>> engine.activate('bc_example')
    >>> 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.

Backward-Chaining Defined
==============================

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
goal.

Backtracking
=====================

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_
    fails.

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_
