Special cases and substitutes for rigid E-unification

The simultaneous rigid E-unification problem arises naturally in theorem pr oving with equality. This problem has recently been shown to be undecidable . This raises the question whether simultaneous rigid E-unification can use fully be applied to equality theorem proving. We give some evidence in the affirmative, by presenting a number of common special cases in which a deci dable version of this problem suffices for theorem proving with equality. W e also present some general decidable methods of a rigid nature that can be used for equality theorem proving and discuss their complexity. Finally, w e give a new proof of undecidability of simultaneous rigid E-unification wh ich is based on Post's Correspondence Problem, and has the interesting feat ure that all the positive equations used are ground equations (that is, con tain no variables).