Negative Paramodulation http://www.ksl.stanford.edu/software/IW/registry/SRC/IW-TEAM.daml Fri Feb 07 11:05:08 PST 2003 Fri Feb 07 12:58:43 PST 2003 "The inference rule negative paramodulation reasons from negated equalities rather than equalities. The rule is sound if the functions involved satisfy certain cancellation-like properties. For example, from A<>B and AC=D, we can derive BC<>D by negative paramodulation provided that right cancellation holds for product."