Demodulation

• If an OTTER input file has a list of demodulators, all terms of newly generated clauses are examined for possible demodulation.
• A term t is demodulated if a demodulator exists such that one of the arguments of the demodulator can be unified with the term without replacing any of the variables in t.
• The usual convention is to consider only the first argument t₁ in the demodulator t₁ = t₂ under consideration for unification with the term under consideration.
• The demodulated term t is obtained by replacing t with the second argument t₂ in the demodulator t₁ = t₂ after variable replaced is applied through unification.
• Then the original version of the clause is replaced by the demodulated version.
• When a new demodulator is found, all clauses previously kept are examined for demodulation with this new demodulator. This first demodulation may in turn lead to iteration of the process.

Paramodulation	Demodulation
original clause retained	original clause discarded
var substitution unrestricted	var substitution restricted
equality literal ``anywhere"	equality literal in unit clause
stops after single application	automatically triggers further attempts