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',)