http://www.ksl.stanford.edu/software/IW/registry/SRC/IW-TEAM.daml Fri Jan 17 17:59:00 PST 2003 Fri Feb 07 13:20:32 PST 2003 "The demodulation rule takes an equality statement x = y and any sentence with a nested term that unifies with x and derives the same sentence with y substituted for the nexted term." "If b.a=c is inferred in the presence of (x^(-1))^(-1)=x, substitution immediately yields obviously related inferences such as (b^(-1))^(-1).a=c." {p1,...,pm}{u<-v}t {p1,...,pm}