Substitution strategies [in proofs]

With the setup I am using each step in a proof involves transforming an expression like u  v using an expression like s  t. And for this to happen s or t must match some part w of u or v. The simplest way this can be achieved is for s or t to reproduce w when its variables are replaced by appropriate expressions. But in general one can make replacements not only for variables in s and t, but also for ones in w. And in practice this often makes many more matches possible. Thus for example the axiom a ∘ a  a cannot be applied directly to (p ∘ q) ∘ (p ∘ r)  q ∘ r. But after the replacement r  q, a ∘ a matches (p ∘ q) ∘ (p ∘ r) with a  p ∘ q, yielding the new theorem p ∘ q  q ∘ q. These kinds of substitutions are used in the proof on page 810. One approach to finding them is so-called paramodulation, which was introduced around 1970 in the context of automated theorem-proving systems, and has been used in many such systems (see page 1157). (Such substitutions are not directly relevant to Mathematica, since it transforms expressions rather than theorems or equations. But when I built SMP in 1981, its semantic pattern matching mechanism did use essentially such substitutions.)