General algorithms for permutations in equational inference (Q5931113)

A problem that frequently arises in theorem-proving applications of term-rewriting systems and equational reasoning is that many permutations of a given term or equation are often produced. There are some methods to deal with this problem. The main idea of the approach presented in this article is not to deal with entire E-equivalence classes of terms, as is done in classical E-unification, but rather to deal with smaller classes that have convenient properties permitting efficient algorithms to be applied. One difference between the proposed method and the usual methods is that one does not always eliminate the equations in E. The authors show how permutation groups arise naturally in equational inference problem. They also study some general algorithms for processing permutations and permutation groups and consider their application to equational reasoning and term-rewriting systems. They show also how these techniques can be incorporated into resolution theorem-proving strategies.