I order to help me understand paramodulation in general I am trying to understand the particular Prover9 example below. Prover9 is an automated theorem prover for first-order and equational logic that uses paramodulation and resolution.
In the Prover9 output below there are three axioms on lines 1, 2 and 3. The theorem to be proved, or goal, appears on line 4. The axioms are transformed into clausal form on lines 5, 6, and 7. The goal is negated on line 8. The negated goal will be used for the resolution on line 19. The justification for the derivation of each line appears in square brackets at the end of the line. According to the Prover9 glossary:
A paramodulation inference consists of two parents and a child. The parent containing the equality used for the replacement is the from parent or the from clause, the equality is the from literal, and the side of the equality that unifies with the term being replaced is the from term. The replaced term is the into term, the literal containing the replaced term is the into literal, and the parent containing the replaced term is the into parent or into clause.
I do not understand the derivation of line 9. Intuitively, I can see that line 9 is the child of parent lines 5 and 6. From the axioms the left sides of both lines can be equated. I will call this equality 9a.
9a turn(move(turn(move(turn(move(turn(move(x)))))))) = turn(turn(turn(turn(x))))
Now line 9 has the first terms, turn(...) ,on the left and right of the equality in 9a removed. The left and right of line 9 are subterms of the left and right of line 9a.
9 move(turn(move(turn(move(turn(move(x))))))) = turn(turn(turn(x))). para(6(a,1),5(a,1,1,1,1)),flip(a)].
From my, perhaps incorrect, view of equational reasoning, from two terms $a$ and $b$ with $a=b$ we can conclude $turn(a) = turn(b)$. From my naive view this reasoning would allow to go from 9 to 9a, but not the other way around.
At the moment, I am not too concerned the other lines of the proof. Any explanation of of how line 9 was inferred would be appreciated.
Prover9 output
1 (all p turn(turn(turn(turn(p)))) = p) # label(non_clause). [assumption].
2 (all p turn(move(turn(move(turn(move(turn(move(p)))))))) = p) # label(non_clause). [assumption].
3 (all p turn(turn(move(turn(turn(move(p)))))) = p) # label(non_clause). [assumption].
4 (all p turn(turn(turn(move(turn(move(p)))))) = move(turn(turn(turn(move(turn(p))))))) # label(non_clause) # label(goal). [goal].
5 turn(turn(turn(turn(x)))) = x. [clausify(1)].
6 turn(move(turn(move(turn(move(turn(move(x)))))))) = x. [clausify(2)].
7 turn(turn(move(turn(turn(move(x)))))) = x. [clausify(3)].
8 move(turn(turn(turn(move(turn(c1)))))) != turn(turn(turn(move(turn(move(c1)))))). [deny(4)].
9 move(turn(move(turn(move(turn(move(x))))))) = turn(turn(turn(x))). [para(6(a,1),5(a,1,1,1,1)),flip(a)].
11 move(turn(turn(move(x)))) = turn(turn(x)). [para(7(a,1),5(a,1,1,1)),flip(a)].
12 move(turn(move(turn(move(turn(turn(turn(x)))))))) = turn(move(x)). [para(11(a,1),9(a,1,1,1,1,1,1,1)),rewrite([5(13)])].
16 move(turn(move(turn(move(x))))) = turn(move(turn(x))). [para(5(a,1),12(a,1,1,1,1,1,1))].
18 move(turn(turn(turn(move(turn(x)))))) = turn(turn(turn(move(turn(move(x)))))). [para(16(a,1),11(a,1,1,1,1))].
19 $F. [resolve(18,a,8,a)].
The example concerns a robot moving through a grid from VanHorebeek and Lewi also in book. Here is related paramodulation post.
Paramodulation is used in Resolution proof procedure with equlity (see e.g. Chin-Liang Chang & Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving (Academic Press, 1973), Ch.8.3 Paramodulation, page 168.
In a nutshell, it is first order logic with equality, using transitivity of $=$ and the substitution propereties.
Consider step 5) $turn(turn(turn(turn(x)))) = x$. It amounts to saying that four times "$turn$" is an identity operation.
Thus, applying three times "$turn$" to 6) and using the substitution for functions axiom, what we get is:
Now we can delete the four "outer" occurrences of "$turn$" in the LHS to get:
[More formally, this means that from 5) $turn(turn(turn(turn(x)))) = x$ and $turn(turn(turn(turn(expr_1)))) = expr_2$ we substitute $x$ with $expr_1$ in 5) to get $turn(turn(turn(turn(expr_1)))) = expr_1$ and using transitivity with the second equation we get $expr_1 = expr_2$, i.e. 9).]
The same for step 11), derived from 5) and
Applying "$turn$" twice to 7) we get:
Now we can delete the four "outer" occurrences of "$turn$" in the LHS to get: