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 .
Equality Resolution
\[
\frac{C \cup \{ s \neq s' \}}
{subst(\sigma)(C)}
\]
where is mgu of .
Completeness of Rules
How would you prove these rules are complete given Herbrand-like theorem for FOL with equality?
Derive axioms for equality.
References