unify

• Params: pat1, pat2, substitution
  substitution a set of variable bindings:
  ((?x 3) (?y ?z) (?z (drop and add)))
• If pat1 and pat2 are equal?, return substitution
• Else if pat1 or pat2 is a variable, call unify-var
• Else if either pat1 or pat2 is an atom, return #f
• Else the patterns are both lists.
  Call unify on corresponding parts of pat1 and pat2.
  • if #f results, return #f immediately.
  • else a substitution results; replace substitution with this and continue.
  Return the final substitution.

unify-var

• Params: var, pat, substitution
• If var has a binding in substitution, call unify with the new value and pat
• Else apply the substitution to pat. If var appears anywhere in the result of the substitution, return #f.
• Else add the binding var = pat to substitution, and return the new substitution.

Examples of Unification

• (drop ?x ?y)
  (drop arnold b552)
  () -->
  ((?x arnold) (?y b552))
• (drop ?x ?y)
  (pickup ?x ?y)
  () -->
  #f
• (drop ?x ?y)
  (drop arnold b552)
  ((?y c511)) -->
  #f
• (drop ?x ?y)
  (drop arnold (class csci 552))
  ((?x ?z)) -->
  ((?x ?z) (?z arnold) (?y (class csci 552)))
• (drop arnold ?x)
  (drop arnold (class ?y 552))
  ((?y ?z) (?z ?x)) -->
  #f

Forward Chaining, Depth-First

For each rule,

• Each state consists of the antecedents left to satisfy and the current variable bindings (the substitution).
• goal-state?: If a state has no more antecedents to satisfy, a goal state has been reached. Add the consequent instantiated with the substitution to working memory.
• extend:
  • Let antec be the instantiation (using substitution) of the first of the antecedents.
  • For each assertion in working-memory,
    • If antec unifies with assertion given substitution, create a new state with the remaining antecedents, the consequent, and the new substitution resulting from the unification.
    • Else return #f.
  • If all assertions resulted in #f, return ().
  • Else return the new states.

Backward Chaining, Depth-First

• Each state consists of the goals left to satisfy and the current substitution.
• goal-state?: If a state has no more goals to satisfy, a goal state has been reached. Return the substitution and/or add the top-level goal instantiated with the substitution to working memory.
• extend:
  • Let goal be the instantiation (using substitution) of the first of the goals.
  • For each assertion in working-memory,
    • If goal unifies with assertion given substitution, create a new state with the remaining goals and the new substitution resulting from the unification.
    • Else return #f.
  • For each production,
    • Assign all of the variables in the production unique names.
    • If goal unifies with the consequent of the rule, given substitution, create a new state with the remaining goals plus the antecedents of the rule and the new substitution resulting from the unification.
    • Else return #f.
  • If all assertions and productions resulted in #f, return ().
  • Else return the new states.