- The paper as published in AICOM has an error in the condition part of
  the inference rule for Clause Subsumption (CS) on the 5th page of the
  paper.

  The rule was written as

  T    R v S
  ==========  if \sigma(S)=T for a substitution \sigma
      T

  It should be

  T    R v S
  ==========  if \sigma(T)=S for a substitution \sigma
      T


- The original paper contained a mistaken statement about
  the undecidabiliy of tautology testing for equational
  clauses. Thanks to Jasmin Blanchette for catching this.

- In the rule RP (Rewriting of positive literals), the side condition
  was stated as "...is not eligible for resolution...", but should be
  "...is not eligible for paramodulation...". This bug was noted by
  Simon Cruanes.


These errors have been fixed in the version published on my private
bibliography page.



- StS