反向链接
反向链接算法从目标开始反向运行，链接规则以找出支持证明的已知事实。反向链接算法是一种与或搜索，其关键在于其的三个核心函数：
$Ask$：实现为生成器，也就是能多次返回的函数，每次返回值给出一个可能的结果（询问成立的置换）。
$Or$：或的部分是由于目标查询可以用知识库中的任意规则证明，工作方式是抓取所有可能与目标合一的子句，将子句中的变量标准化为全新变量，如果子句确实能够与目标合一，就使用$And$证明所有合取子句。
$And$：证明前件中的所有合取子句。这个函数的工作方式是轮流证明合取子句，并记录运行中积累的所有置换。
反向链接明显是深度优先搜索算法。这意味着其空间需求与证明规模呈线性关系，也意味着反向链接（不同于前向链接）受制于重复状态和不完备性。尽管有这些局限，事实表明反向链接在逻辑编程语言中仍然是非常流行且有效的。
深度优先搜索和包含了重复状态和无限路径的搜索树之间的错配。反向链接算法会陷入无限路径。因此，作为一个确定子句的定理证明器，反向链接是不完备的，因为对于某些知识库，它无法证明其所蕴含的语句。深度优先反向链接也有冗余计算的问题，大部分推断用于找出到达无法达成目标的节点的所有可能路径。这类似于之前所述的重复状态问题。推断的总量随着生成的基本事实的数量增加而呈指数增长。
图搜索问题中的前向链接是动态规划的一个实例，其子问题的解是由更小的子问题的解递增构建的，通过缓存更小的子问题来避免重复计算。可以在反向链接中达到类似的效果，只需要将大目标分解为小目标而非从小目标构建大目标。不论如何，存储中间结果以避免重复计算是问题的关键。这是表格化逻辑编程系统所采取的方法，它使用高效的存储和检索机制。表格化逻辑编程结合了反向链接的目标导向性以及前向链接动态规划的高效性。它对于数据日志知识库是完备的，这意味着程序员不太需要为死循环而担忧。（使用指代可能有无穷多对象的语句时，它仍然可能会进入死循环。）
归结
逻辑系统家族中的最后一个成员，也是唯一能够用于所有知识库而不仅是确定子句的成员，是归结。
合取范式（$CNF$）——每个子句为文字析取的子句合取式。在$CNF$中，文字可以包含变量，假定这些变量是全称量化的。每条一阶逻辑语句都可以转换为推断上等价的$CNF$语句。
（1）蕴含消去：
$$
\alpha \Rightarrow \beta \equiv \lnot \alpha \lor \beta
$$
（2）$\lnot $内移：
$$
\lnot \forall x\ p\equiv \exists x\ \lnot p
$$
$$
\lnot \exists x\ p\equiv \forall x\ \lnot p
$$
（3）变量标准化：对于两次使用相同变量名的语句，更改其中一个变量名。这可以避免在消除量词时产生歧义。
（4）斯科伦化：斯科伦化就是通过消去移除存在量词的过程，类似存在量词实例化但是为了保持语义需要一定的改造。不将其实例化为特定实体$A$，而将其实例化依赖于全称量词辖区的$x$的函数$F(x)$，$F$是斯科伦函数。总的规则是，斯科伦函数的参数全部是全称量化的变量，要消去的存在量词出现在这些变量的辖域内。与存在量词实例化一样，斯科伦化的语句的可满足性与原始语句完全一致。
（5）全称量词消去：此时，所有剩余变量必然是全称量化的，直接消去量词即可。
（6）对$\land $分配$\lor $：展开再合并为析取句的合取式。
通过这些处理，语句成为了含有多个子句的$CNF$。它比原本含有蕴涵的语句难读多了。幸运的是，人类很少需要考察$CNF$语句——翻译过程很容易自动化。
一阶逻辑下的归结规则为：
$$
\frac{\ell _1\lor \cdot \cdot \cdot \lor \ell _k,\,\,\,\,\,\,m_1\lor \cdot \cdot \cdot \lor m_n}{Subst\left( \theta ,\ell _1\lor \cdot \cdot \cdot \ell _{i-1}\lor \ell _{i+1}\cdot \cdot \cdot \lor \ell _k\lor m_1\lor \cdot \cdot \cdot m_{j-1}\lor m_{j+1}\cdot \cdot \cdot \lor m_n \right)}
$$
其中$Unify\left( \ell _i,m_k \right) =\theta $；上式通过合一子来消去互补文字，生成归结式子句。这个规则叫作二元归结规则，因为它刚好归结两个文字。二元归结本身并不产生完备的推断过程。完备的归结规则能够归结每个子句的可合一文字子集。另一种方法是将因子提取（也就是对冗余文字的消除）拓展到一阶逻辑。命题逻辑因子提取将两个相同的文字约简为一个，一阶逻辑因子提取则约简两个可合一的文字。这种合一子必须应用于整个子句。二元归结和因子提取的组合是完备的。遗憾的是，归结有时会对存在量化目标产生非构造性证明，即知道一个查询为真，但却不知道这个变量的唯一绑定。
目前为止所有推断方法都不能在不增加额外工作的情况下处理形如$x = y$的断言。为此可以采取 3 种不同的方法。
第一种方法是公理化等词，也就是在知识库中写入相等关系的语句。由于相等是自反的、对称的和传递的，同时对任意谓词或函数中用相等量置换相等量。因此需要 3 类基本公理，另外每个谓词和函数都需要一条公理：
给定这些语句，标准的推断过程，如归结，就可以执行需要等词推理的任务，如求解数学方程。不过，这些公理会产生大量结论，其中大多数对证明没有帮助。
第二种方法是添加推断规则而非公理。最简单的规则是解调，它取单元子句$x = y$和一个含有$x$项的子句，生成一个用$y$置换$\alpha $中的$x$得出的新子句。如果$\alpha $中的项能够与$x$合一，解调就可以使用，而不需要完全等于$x$。注意，解调是有方向性的，给定$x = y$，$x$总是会被$y$替换，而非相反。更为形式化地，有:
解调：对于任意项$x$、$y$和$z$，其中$z$出现在文字$m_i$中的某处且$Unify\left( x,z \right) =\theta \ne failure$，则有：
$$
\frac{x=y\ ,\ m_1\lor \cdot \cdot \cdot \lor m_n}{Sub\left( Subst\left( \theta ,x \right) ,Subst\left( \theta ,y \right) ,m_1\lor \cdot \cdot \cdot \lor m_n \right)}
$$
其中$Subst$是对绑定表的一般置换，而$Sub(x,y,m)$表示在$m$中的某处用$y$替换$x$。
这个规则可以拓展到处理含有等词的非单元子句：
超解调：对于任意项$x$、$y$和$z$，其中$z$出现在文字$m_i$中的某处且$Unify\left( x,z \right) =\theta \ne failure$，则有：
$$
\frac{\ell _1\lor \cdot \cdot \cdot \lor \ell _k\lor x=y\ ,\ m_1\lor \cdot \cdot \cdot \lor m_n}{Sub\left( Subst\left( \theta ,x \right) ,Subst\left( \theta ,y \right) ,Subst\left( \theta ,\ell _1\lor \cdot \cdot \cdot \lor \ell _k\lor m_1\lor \cdot \cdot \cdot \lor m_n \right) \right)}
$$
超解调产生含有等词的一阶逻辑的一个完备推断程序。
第三种方法仅使用拓展的合一算法处理等词推理。也就是说，如果若干项在某种置换下可证明为相等，则它们是可合一的，其中“可证明”允许等词推理。例如，项$1 + 2$和$2 + 1$通常不可合一，但知道$x + y = y + x$的合一算法可以用空置换合一它们。这种等词合一可以用针对特定公理（交换性、结合性等）设计的高效算法完成，而非通过直接用这些公理推断。
只要证明存在，反复运用归结推断规则总会找到一个证明，但是是否存在有助于高效找出证明的策略呢？答案是肯定的。
1、单元优先：这个策略优先处理其中一条语句为单文字（也就是单元子句）的归结。这一策略的思路是，希望产生空子句，因此先处理产生较短子句的推断可能是个好主意。当这种单元优先策略在 1964 年首次被用于命题推断时，它产生了巨大的加速作用，使得它能够证明许多先前无法处理的定理。单元归结是归结的一种受限形式，其中归结的每一步都含有单元子句。单元归结总体上是不完备的，但对霍恩子句是完备的。霍恩子句上的单元归结证明与前向链接类似。
$Otter$定理证明器（$McCune$, $1990$）使用了最佳优先搜索。其启发函数度量每个子句的“权重”，并偏好权重较轻的子句。启发式函数的选择取决于用户，但通常子句的权重应当与其规模或难度相关。它认为单元子句权重较轻，因此这种搜索可以被看作单元优先策略的一般化。
2、支撑集：优先尝试某些归结是有用的，但一般来说一起消除某些有潜力的归结是更为高效的做法。例如，可以使每个归结步都用到一个特殊子句集的至少一个元素，这个特殊子句集就是支撑集。归结式随后被加入支撑集中。如果支撑集远小于整个知识库，则搜索空间会大大简化。为确保这种策略的完备性，可以选择使得语句的剩余部分同时可满足的支撑集$S$。例如，假设原始知识库是一致的，就可以使用否定查询作为支撑集（毕竟，如果知识库不一致，则查询符合知识库也没什么意义了）。支撑集策略还有一个好处，它能够生成目标导向的证明树，利于人类理解。
3、输入归结：这种策略中，每个归结都是一个输入语句（来自知识库或查询）与其他一些语句的结合。因而具有单条“主线”且单条语句向主线结合的结构特征。显然，这种证明树的空间小于整个证明图的空间。
在霍恩知识库中，肯定前件是一种输入归结策略，因为它将原知识库中的一个蕴涵式与其他语句结合。因此，知道输入归结对于霍恩形式的知识库是完备的，但一般情况下它是不完备的。如果$P$在原始知识库中或$P$在证明树上是$Q$的祖先的话，线性归结策略允许$P$和$Q$一同归结。线性归结是完备的。
4、包容：包容方法消除所有知识库中已有语句所包含的语句（也就是更为精确的语句）。包容能够使知识库较小，进而有助于减小搜索空间。
5、学习：可以通过从经验中学习改进定理证明器。给定先前证得的定理集，训练机器学习系统来回答问题。
