What is the difference between superposition and paramodulation?

I am currently writing a paper about automated theorem proving in first-order logic. Equality is not uncommon for mathematical problems and almost every theorem prover like VAMPIRE or SPASS has a calculus for equality. But the most paper are always writing about the term "superposition" calculus. A simple google search did not help to find any information about this term, only the wikipedia website which means "it can be used for first-order logic with equality".

Another paper referneced to the Paramodulation-based theorem proving which describes the concept of paramodulation for theorem proving. It seems that the superposition is some modified version of paramodulation, but I don't understand why and in which way.

So, is there any explanation of this calculus or can someone give me some hints what is different from paramodulation?

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

StackExchange Computer Science Q#49881, answer score: 5