# Proving Goals

Though Pyke has the capability to return multiple answers to a single goal, often you just want the first answer:

some_engine.prove_1_goal(goal, **args)

  `goal` is a Pyke goal (as a string). This may include pattern variables (which start with a '$').

      >>> my_engine.prove_1_goal('bc_related0.father_son(thomas, david, $depth)')
      ({'depth': ('grand',)}, None)

  Returns the first proof found as a 2-tuple: a dict of bindings for the pattern variables, and a plan. The plan is `None` if no plan was generated; otherwise, it is a Python function as described here.

> Args must be specified as keyword arguments and are set as the value of the corresponding pattern variable.

>     >>> vars, plan = \
>     ...   my_engine.prove_1_goal('bc_related0.father_son($father, $son, $depth)',
>     ...                          father='thomas',
>     ...                          son='david')
>     >>> sorted(vars.items(), key=lambda item: item[0])
>     [('depth', ('grand',)), ('father', 'thomas'), ('son', 'david')]

> Prove_1_goal raises `pyke.knowledge_engine.CanNotProve` if no proof is found:

>     >>> my_engine.prove_1_goal('bc_related0.father_son(thomas, bogus, $depth)')
>     Traceback (most recent call last):
>         ...
>     CanNotProve: Can not prove bc_related0.father_son(thomas, bogus, $depth)

some_engine.prove_goal(goal, **args)

  This returns a context manager for a generator yielding 2-tuples, as above. Unlike `prove_1_goal` it does not raise an exception if no proof is found:

      >>> from __future__ import with_statement

      >>> with my_engine.prove_goal(
      ...        'bc_related0.father_son(thomas, $son, $depth)') as gen:
      ...     for vars, plan in gen:
      ...         print vars['son'], vars['depth']
      bruce ()
      david ('grand',)

  Like `prove_1_goal`, above, pattern variables in the goal may be specified with keyword arguments:

      >>> with my_engine.prove_goal(
      ...        'bc_related0.father_son($father, $son, $depth)',
      ...        father='thomas') as gen:
      ...     for vars, plan in gen:
      ...         print vars['son'], vars['depth']
      bruce ()
      david ('grand',)

## Compiling Goals at Program Startup

Similar to Python's regular expression library, `re`, you may compile your goal statements once at program startup:

>     >>> from pyke import goal

>     >>> my_goal = goal.compile('bc_related0.father_son($father, $son, $depth)')

Then use `my_goal.prove_1` and `my_goal.prove` as many times as you'd like:

>     >>> vars, plan = my_goal.prove_1(my_engine, father='thomas', son='david')
>     >>> sorted(vars.items(), key=lambda item: item[0])
>     [('depth', ('grand',)), ('father', 'thomas'), ('son', 'david')]

>     >>> with my_goal.prove(my_engine, father='thomas') as gen:
>     ...     for vars, plan in gen:
>     ...         print vars['son'], vars['depth']
>     bruce ()
>     david ('grand',)

Copyright © 2007-2009 Bruce Frederiksen

Page last modified Tue, Mar 09 2010.