Equality elimination is a method of handling equality in automatic
theorem proving. Unlike the known paramodulation-based methods,
it is also applicable to rigid-variable methods (tableaux and
connections). In the case of the tableau method, equality elimination
results in a combination of backwards reasoning by the tableau method
and forward superposition-based reasoning.
In the talk, we shall describe the method and briefly survey other
methods of equality reasoning for rigid-variable methods.
All reported results have been obtained in collaboration with Anatoli
Degtyarev.