The rule-utils.scm defines the basic data structures and operations used in the forward and backward chainers; see the description. Please read about the format of rules (aka "knowledge") files. Note, in particular, that variables in the rules can be written as ?x or (? x) as you prefer.

The backward.scm file defines the backward-chainer with variables (using unify). As this is a bit difficult to follow, the file backward-simple.scm implements a backward-chainer without variables. The basic control structure is much easier to see in the simple implementation.

The rules used by the backward chainer are in the same format as those used by the forward-chainer. Excepth that only the IF, AND-IF and THEN keywords are supported. Also, the backward chainer can only handle rules with a single THEN clause.

The top-level chaining operation can be initiated in one of three modes:

• (backchain-asking-user goal) - in this mode, the user is asked for the truth of a goal if it cannot be established otherwise. Only goals with no variables are queried. Chaining stops when the goal is first established.
• (backchain-all goal) - in this mode, chaining does not stop when the goal succeeds. Chaining continues to find other instantiations of the goal that may also succeed. The user is not queried in this mode.
• (backchain goal) - in this mode, the user is not queried and the chaining stops when the goal is first established.

(read-k-file "/mit/6.034/www/psets/ps3/zoo.k")
(backchain-asking-user '(splashy is a ?what))
(display-assertions)