2.2.6 等词推理
相等是数学中的重要且常用的概念之一，使用一阶逻辑来描述表达数学定理时经常需要使用相等这个二元谓词，下文中用=表示等词， s=t，实际上表示=(s,t)，用≠表示=。对于包含等词的子句集 S，若S是不可满足的，使用归结原理不能找到从 S 推出空子句的演绎。这是
因为在应用归结原理的符号系统里，代表等词的=就是普通的二元谓词，在解释中可以被指定为任意的二元谓词，并不是一定会被指定为表示相等的谓词。在这种观点下，子句集 S 有可能是可满足的，使用归结原理不能找到从 S 推出空子句的演绎。
为了对包含等词的问题进行推理，一种直接的方法是增加公理集合 K：
(1) x=x （反身性）
(2) x≠yy=x （对称性）
(3) x≠yy≠zx=z （传递性）
(4) xj≠x0P(x1,...,xj,...,xn)P(x1,...,x0,...,xn) j=1,2,...,n, P(x1,...,xn)
是 S 中任意的n 元谓词符号 （等量代换）
(5) xj≠x0f(x1,...,xj,...,xn)=f(x1,...,x0,...,xn) j=1,2,...,n, f(x1,...,xn)是 S 中任意的n 元函数符号 （等量代换）
对于包含等词的子句集 S，若 S 是不可满足的，则存在从 SK推出空子句的演绎。这种方法的缺点是输入的子句集合增大，应用归结原理的过程中将生成更多的无用子句，效率降低。
另外一种方法是设计专门的推理规则来处理等词的推理。下面介绍调解法[86] ，其本质上是等量替换规则的推广。
以基情况为例，若子句 C1 和C2 分别为 L[t]C1’和t=sC2’，其中 L[t]表示包含项 t 的文字，C1’和 C2’是子句，于是 L[s]C1’C2’称为 C1和 C2 的调解式。
在一般子句上，例如
C1: P(x)Q(b)
C2: a=bR(b)
尽管 C1 中不包含 a，但替换{a/x}作用在 C1 上得到 C1 的例包含
a，于是可以和 C2 进行调解，得到 P(b)Q(b)R(b)。
调解法提出以后，和归结方法一样，为提高其效率，很多改进方
法被提出来。例如：支撑集调解法，线性调解法，P 超调解[84] 等。设 P 是子句 C1 和 C2 中谓词符号的一个次序，C1 和 C2 的一个调
解式称为P 超调解式，当且仅当满足条件：C1 和C2 是正子句；C1 和
C2 中的调解文字分别是 C1 和C2 中最大谓词符号。
从 S 出发使用归结和调解的 P 超演绎是一个子句序列，其中的每个子句或者来自S，或者是一个 P 超归结式，或者是一个 P 超调解式。对于含等词的不可满足子句集 S，存在从 S{x=x}F 推出空子句的 P 超演绎，其中 F 是关于 S 中出现的全部函数符号的反身公理集。
1973 年，Chang, C. L.和 Lee，R. C. T.出版了人工智能领域颇具影响力的专著《Symbolic Logic and Mechanical Theorem Proving》[84] 。 1990 年，吉林大学刘叙华团队发现该专著中关于输入调解和单元调解等价性的猜测是错误的，并发现 Chang 和 Lee 在定义调解和使用调解时，存在着某种含混，从而导致一批引理和定理都可能是错误的，甚至线性调解的完备性都可能是错误的。为此，引入了对称调解的概念，使得 Chang 和 Lee 著作中的所有含混之处都变得明确起来，并进一步指出了调解和对称调解各自的优缺点[102] 。
后来，从调解法又发展出 superposition 方法，这是当前主流的等词推理方法[87] 。引入项的次序，要求等量替换时只能对排序在前的项应用，进而减少新生成的文字。例如，对于等词 s[l]=t 和l=r，只有当 s>t, l>r 时，才能用 r 替换 l 得出 s[r]=t，其中 s[l]表示包含项 l 的项。