First-Order Disunification
一阶反合一研究

文章讨论一阶反合一问题以及求反合一子完备集的算法.在合一问题中,有多种求解合一问题的方法,其中研究得较为彻底的是用转换规则进行求解的方法.在研究反合一问题的过程中,人们也陆续提出了许多转换规则,这样做的结果是最终给出的是已解出形.该文在已解出形的基础上讨论一种方法，以给出具体解的完备集（反合一子完备集）.通过引入Gθ和Z函数，使求解更为方便、直观.