This is late for you, but probably might be of help to others. I myself had asked this question and I wrote the summary of my findings to the acl2-help mailing list on 8 and 9 September 2013: https://utlists.utexas.edu/sympa/arc/acl2-help/2013-09/msg00005.html
https://utlists.utexas.edu/sympa/arc/acl2-help/2013-09/msg00006.html
Disclaimer: What follows is my understanding of the subject and I am not an expert.
I assume you are familiar with what is called
term-rewriting. Informally its a very simple notion where one uses a
rule to reduce or rewrite another expression.
A rewrite rule is usually a universally quantified formula of the form
$C \Rightarrow l=r$, where $C$ is a formula and $l$ and $r$ are terms. One says that a
rule $R$ applies to another formula $\Phi$, if there is some subterm $s$ of
$\Phi$ and some substitution $\sigma$ such that $l\sigma = s$ (this process
is called matching) and $C\sigma$ is true. If $R$ applies to $\Phi$, then
one can rewrite $\Phi$ to $\Phi\sigma$. Demodulation is another name for
unconditional term-rewriting, i.e., $C$ is simply true and so $R$ is just
$l=r$.
Rewriting involves matching,i.e., one-way unification.
Paramodulation involves full unification. Moreover, the equality
($l=r$) that is used to perform paramodulation, is not directed, either
lhs or rhs can be unified with a subterm in the other literal
paramodulated upon.
Superposition is a restriction of Paramodulation. In particular, the
rules of inference named 'Superposition (left/right)' are restrictions
of "ordered" paramodulation, i.e., the paramodulation rule is applied
only when equation $l=r$ (to be instantiated/unified) satisfies certain
properties: $l >> r$ for a given reduction order $>>$, $l=r$ is maximal (wrt
$>>$) in the clause etc etc.
Here are some fundamental papers that are interesting from a historical point of view.
[1] The concept of demodulation in theorem proving - L Wos, GA
Robinson, DF Carson, L Shalla - Journal of the ACM (JACM), 1967
[2] Handbook of Logic and Automated Reasoning - J Harrison.
[3] Paramodulation and theorem-proving in first-order theories with
equality- G Robinson, L Wos - Machine intelligence, 1969
[4] Rewrite-based equational theorem proving with selection and
simplification - L Bachmair, H Ganzinger - Journal of Logic and
Computation, 1994
[5] Simple word problems in universal algebras - DE Knuth, PB Bendix -
Computational problems in abstract algebra 1970
[6] A superposition oriented theorem prover - L Fribourg - Theoretical
Computer Science, 1985 - Elsevier
[7] Completion without failure - L Bachmair, N Dershowitz, DA Plaisted -1989
