LARA

Proof Rules for Equality

Paramodulation

\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$.

Equality Resolution

\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.

Completeness of Rules

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

References