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 .