A simple, yet non-superficial explanation of what "paramodulation" means in the context of automated theorem proving?

Question

Modern automated theorem provers seem to be paramodulation-based.

I only have a superficial understanding of what this means: we derive a proposition whose truth is implied from the truth of [two?] other propositions.

Q: What is a simple, yet non-superficial explanation of what "paramodulation" means in the context of automated theorem proving?

Looking up the definition in papers invariably reveals a mountain of jargon and notation, which frightens me off. (A Wikipedia page for paramodulation does not exist yet: link.) Besides, I find that a non-superficial understanding of topics requires seeing through the notation and getting a "feel" for what it means.

Here's a first-order-logic proof that Boolean groups (groups for which $x^2=e$ for all $x$) are abelian (sourced from Robinson, Wos, Paramodulation and Theorem-proving in First-Order Theories with Equality [pdf]):

\begin{align*} 1. & & & f(ex)=x \\ 2. & & & f(xe)=x \\ 3. & & & f(xf(yz))=f(f(xy)z) \\ 4. & & & f(xx)=e \\ 5. & & & f(ab)=c \\ 6. & & & c \neq f(ab) \\ 7. & & & f(xe)=f(f(xy)y) & \text{4. into 3. with } \delta:f(yz) \\ 8. & & & x=f(f(xy)y) & \text{2. into 7. on } f(xe) \\ 9. & & & a=f(cb) & \text{5. into 8. on } f(xy) \\ 10. & & & f(yf(yz))=f(ez) & \text{4. into 3. on } f(xy) \\ 11. & & & f(yf(yz))=z & \text{1. into 10. on } f(ez) \\ 12. & & & f(ca)=b & \text{9. into 11. on } f(yz) \\ 13. & & & c=f(ba) & \text{12. into 8. on } f(xy) \\ 14. & & & \square & \text{resolved with 6.} \end{align*} We can see 1. through 3. are some of the group axioms, 4. is the Boolean property, and 5. is used to form a proof by contradiction. And the 7. through 14. can be deduced as indicated (using substitution, renaming variables, and "multiplying" both sides of the equation).

Answer 1

Do you know about the refutation theorem-proving technique of resolution?

The resolution rule is refutation-complete, in that a set of clauses is unsatisfiable if and only if there exists a derivation of the empty clause using resolution alone.

Paramodulation is the modification of resolution system to manage equality.

You can see detailed treatments of resolution into Melvin Fitting, First-Order Logic and Automated Theorem Proving (1990) [for paramodulation: page 231] or Chin-Liang Chang & Richard Char-Tung Lee, Symbolic Logic and Mechanical Theorem Proving (1973) [for paramodulation: page 168].

From Chang & Char-Tung Lee, page 168:

Consider the following clauses

$C_1 : P(a)$

$C_2 : a = b$.

Since $C_2$ is an equality $a = b$, we substitute $b$ for $a$ in $C_1$ to obtain a clause

$C_3 : P(b)$.

In general, the equality substitution rule can be stated as follows: If a clause $C_1$ contains a term $t$ and if a unit clause $C_2$ is $t = s$, then infer a clause by substituting $s$ for one single occurrence of $t$ in $C_1$.

Paramodulation is essentially an extension of the above equality substitution rule. It can be applied to any pair of clauses (not necessarily unit clauses). For convenience, if an expression $E$ (for example, a clause, a literal, or a term) contains a term $t$, we shall sometimes denote $E$ by $E[t]$. Also, if one single occurrence of $t$ is replaced by a term $s$, the result will be denoted by $E[s]$. By this convention, paramodulation for ground clauses can now be stated as follows: If $C_1$ is $L[t] \lor C_1^*$, where $L[t]$ is a literal containing a term $t$, and $C_1^*$ is a clause, and if $C_2$ is $t = s \lor C_2^*$, where $C_2^*$ is a clause, then infer the following clause, called a paramodulant :

$L[s] \cup C_1^* \cup C_2^*$.