> What are demodulation and paramodulation? How are they different, if at
> all?

pedrito's (summary) answer
--------------------------
they are rules of inference for FOL with equality, thus avoiding the
unattractive alternative of supplying substitution axioms. paramodulation
with resolution is refutation complete for fol with equality, whereas
demodulation is more efficient and easier to understand. 

patrick's (more detailed) answer
--------------------------------
Paramodulation is a rule of inference allowing us to make refutation 
resolution complete even when there is equality.  Demodulation is a 
weaker form of paramodulation (not complete) that is also easier to 
compute.  

The idea behind both rules is that we should be able, when doing 
resolution, to do substitutions involving one variable in place of 
another when the two variables are known to be equal.  As R&N put it, 
"the demodulation rule takes an equality statement x = y and any sentence 
with a nested term that unifies with x and derives the same sentence with 
y substituted for the nexted term."

The difference is that demodulation only deals with equality sentences of 
the form "x = y," while paramodulation can handle sentences with less 
complete information, for example, when we do not know x = y but we do 
know x = y V P(x).


pedrito's (addemdum) answer
---------------------------

here's a bit more detail on the demodulation/paramodulation question
for your enjoyment.

the definition of demodulation is:

	{p1,...,pm}
	{u=v}
	-----------
	{p1,...,pm}{u<-v}t

where pi is a literal, u and v are terms, and t is a variable
renaming.

the definition of paramodulation is:

	{p1,...,pm}
	{u=v,q2,...,qn}
	---------------
	({p1,...,pm}{u<-v} U {q2,...,qn})s

where qi is a literal and s is a most general unifier.

the general application strategy is as follows: (1) apply the rule to all
newly generated clauses; (2) whenever an equation (an equality literal) is
generated, apply it to all previous clauses; (3) in the case of
demodulation, remove the substitutee (i.e. {p1,...,pm}) from the database. 

in terms of complexity, if given k equations, a literal with n arguments,
and the strategy above, an application of demodulation yields at most one
clause where as paramodulation produces (k+1)^n possible clauses. 

thus, demodulation is more efficient. on the other hand, paramodulation is
resolution-complete for fol with equality, whereas demodulation is not. 
the additional power of paramodulation is a result of the following
differences from demodulation: it allows variable substitution in both
arguments of the equation and the substitutee, it does not require the
clause with the equality to be unit, it allows binding of variables
outside of the equation, and it does not delete the substitutee. 

for examples, etc., see genesereth's cs157 class webpage which should be
available via the quail97 homepage.