Deciding the word problem in the union of equational theories sharing constructors

摘要

The main contribution of this paper is a new method for combining decision procedures for the word problem in equational theories sharing "constructors." The notion of constructors adopted in this paper has a nice algebraic definition and is more general than a related notion introduced in previous work on the combination problem.