Errata

• Page 271:
  A condensation D of a clause C is a minimal multiple factor of C which subsumes C. A clause is condensed if there is no proper subclause of C which is a factor of C.
• Page 278, Replace (i) in definition of resolution with maximal selection by:
  \sigma is the most general unifier of A1 \/ ... \/ An and -An+1 \/ ... \/ -A2n such that Ai\sigma = An+1\sigma.
• Page 278, (iii) in definition of resolution with maximal selection:
  Replace Ai by Aj.