Proof Rules for Equality

$\begin{equation*} \frac{D \cup \{ s = t \}\ \ \ \ C[s'] } {subst(\sigma)(D \cup C[t])} \end{equation*}$

where $\sigma$ is mgu of $\{s,s'\}$ .

Here $C[s']$ means that $s'$ occurs somewhere in $C$ ; then $C[t]$ results from replacing that occurrence of $s'$ with $t$ .

$\begin{equation*} \frac{C \cup \{ s \neq s' \}} {subst(\sigma)(C)} \end{equation*}$

where $\sigma$ is mgu of $\{s,s'\}$ .

Superposition: a closely related technique to paramodulation, also meant for dealing with equality.

How would you prove these rules are complete given Herbrand-like theorem for FOL with equality? Derive axioms for equality.

References