This is an old revision of the document!
Proof Rules for Equality
Paramodulation
\[ \frac{D \cup \{ s = t \}\ \ \ \ C[s'] }
{subst(\sigma)(D \cup C[t])}
\] where is mgu of .
Here means that occurs somewhere in ; then results from replacing that occurrence of with .
Equality Resolution
\[ \frac{C \cup \{ s \neq s' \}}
{subst(\sigma)(C)}
\] where is mgu of .
Superposition: a closely related technique to paramodulation, also meant for dealing with equality.