Paramodulation

It was experimentation with P1 that led to Wos's invention of the paramodulation inference rule[22]. Wos began collaboration with George Robinson, who was the principal architect of the next system, called RW1 (``Robinson-Wos 1''). This system was used in the late sixties to experiment with the new paramodulation inference rule as well as demodulation[22]. (This work preceded, but apparently did not influence, the work of Knuth and Bendix, who independently formulated paramodulation and demodulation, and then applied them to the notion of a complete set of reductions in their 1970 paper[5]). RW1 could do the equality versions of the problems P1 could do, as well as showing the dependence of the fourth and fifth axioms in a ternary boolean algebra on the first three axioms. RW1 also had all the capabilities of P1.

One problem that was too hard for RW1 was the ``the commutator problem'', which states that in a group in which x³ = e, [x,y],y] = e, where [x,y] represents the commutator of x and y. Wos had proofs of this theorem, one with binary resolution (138 steps), and another using paramodulation (46 steps), but the problem could not be done automatically using the available technology. One reason was the lack of back demodulation.