Page 249


We'll use the unifier in unify.lisp. It handles circular bindings and uses a list of binding lists, the same as the prover in ddr.lisp,


Always be nervous when code assumes some sequence is non-empty. Can you create a symbol that will cause var? to blow up?

Page 252


Making <- a macro is cute but not very useful. It means there's no easy to load a set of rules stored in a variable.


This function would be better if it were data-driven, with a table linking symbols to proof procedures. That way new special logical forms could be added without editing the basic definition of prove.


Using union on the CAR and CDR is CONSful. Look at the definition of pattern-variables in ddr.lisp for a more efficient approach.


The value returned for a variable with binding is not a very satisfactory if the variable is bound to another variable. See replace-variables in ddr.lisp for an recursive solution that gets to the bottom of a value chain, if possible.