一致化理论在自动推理、自然语言理解、逻辑证明、重写理论等研究领域中有着广泛的应用。目前语法一致化因子的产生算法和工具已经相对成熟,但还没有产生等价一致化因子的实用算法和成熟工具。本文提出并实现了一种构造等价一致化因子产生器的方案：首先,由浅入深的提出了几种语法一致化问题的解决方案,本文从最直观的递归方法开始,然后为了避免重复访问,新的算法中应用了新的数据结构-有向无环图来表示项,用图中的有向边来表示替换。这样我们可以得到一个在平均情况下近似于线性的算法。然而此算法依旧可以优化,方法就是将项的一致化规约问题到等价类的合并问题,并且我们可以在集合的合并中应用按秩合并以及路径压缩策略,这样可以使我们的算法在一般情况下更接近线形；再往后,本文又引入等价一致化的概念,并且将原先语法一致化中问题逐步推广定义到等价一致化,并且在等价一致化中寻找解决方案。为了将语法一致化中的解决方案规约到等价一致化,本文的方法是对相应的等价一致化问题进行调整,把它们转化成几个等价的语法一致化问题的组成的集合。本文中的主要思路是通过项与树形之间的一一对应关系以及对树形进行变换产生对应项的集合,进而也就得到了与原先等价一致化问题等价的由一些语法一致化问题组成的集合；这样一来,我们就可以对此集合中的问题调用已有的解决方案,也就将语法一致化的解决方案扩充到了等价一致化中。这种方法可以求解通常丢番图等式所无法得到的等价一致化因子,因而能够被广泛地应用于实际的科学研究和自动工具中去。在模型检测这个研究领域里,目前已有的安全协议模型检测器的核心便是语法一致化算法,这些检测器使用Dolev-Yao模型来为攻击者的能力建模。然而如果假设攻击者有简单的代数计算能力,则其攻击能力将超过Dolev-Yao模型。而其解决方法便是将核心的语法一致化算法改为等价一致化算法。所以在文中,我们又简要介绍了关于模型检测,和安全协议验证的一些背景。