LARA

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

\[ \frac{C \cup \{ s \neq s' \}} 

   {subst(\sigma)(C)}

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

Completeness of Rules

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

References