Unit Deletion http://www.ksl.stanford.edu/software/IW/registry/SRC/IW-TEAM.daml Fri Feb 07 11:01:58 PST 2003 Mon Mar 31 12:18:23 PST 2003 "Unit Deletion acts rather like demodulation, automatically removing a literal in a clause when a unit clause exists that unifies with the literal, that is opposite in sign, and such that the unification does not affect the variables in the literal in question."