Unification is a procedure that compares two expressions to determine whether some set of legal substitutions exists that can make the two equal. This procedure is used in inference to determine whether to fire a rule. For example, in forward inference, if some set of assertions in the KB matches (can unify with) the antecedent of the rule, we can fire the rule.
