反向链接算法如何在一阶逻辑中工作？

Question

我能否解释一下for each 循环，因为它对我来说没有多大意义。特别是，STANDARDIZE-APART() 和倒数第二行是做什么的？

这是FOL_BC_ASK(KB,[p1...,pn|REST(goals)],COMPOSE(@',@)) U ans

Answer 1

r 是知识库中的一个 FOL 语句。

除其他外，FOL 句子可能包含量词和变量。

对于任何 FOL 句子，都有其简化形式，有多种形式，例如 CNF（连接范式）（喇叭从句类似），该算法对其进行操作。 CNF 风格的简化仅限于特定的、有限的一组运算符，并且通常会导致与原始语句相比扩展语句（有时要长得多）。 CNF 不使用量词，但允许使用变量。

量词是运算符“for-all”（通用）和“there-exists”（存在）。每个量词采用一个变量（或变量列表）和一个（子）语句，在该语句上（在列表中）引入的变量被量化。这些变量被称为是有约束力的，尽管只是针对一个子语句的范围（在量化表达式中）。 因此，量词隐含地引入了一个新的范围（为其变量）。

CNF 不允许显式表达量词，也不为变量提供多个或单独的范围！因此，不仅必须消除量词，而且还必须消除变量的范围（或折叠到单个范围）。 （范围很容易消除，因此首先完成。）

当单个语句包含多个量词时，在 FOL 中完全可以接受在具有不相交范围的量词中重用相同的变量名称。因此，以下单个（尽管是复合）语句在 FOL 中是可接受的：

(there-exists(x) (Father(x,Joe))) AND (there-exists(x) (Mother(x,Joe)))

表示有一些 x 是 Joe 的父亲，还有一些 x（另一个 x）是 Joe 的母亲。

在上面的语句中，变量 x 被引入了两次，尽管它的两种不同用途实际上是无关的！然而，因为 x 被使用了两次，当我们阅读和解释或操作和转换这个语句时，我们必须保持对两个独立范围的了解（否则我们的转换有时会失败）。这对于任何 FOL 语句都是如此，这意味着我们需要了解范围，以便解释和操作一般 FOL 语句。

以下语句从逻辑角度看是等价的，但没有使用两次 x：

(there-exists(x) (Father(x,Joe))) AND (there-exists(y) (Mother(y,Joe)))

如果我们保证我们的（转换后的）语句没有重叠的变量（即在不相交的作用域中没有两次使用相同的变量名），我们不再需要考虑由两种量化的使用引入的两个独立的作用域.我们可以有效地认为此类语句的变量只有一个范围。这是 STANDARDIZE-APART 分离的本质，通过确保跨范围的变量不重叠（通过给它们每个唯一的名称），我们不再需要在单个语句中分别考虑多个范围（可能有多个量词）。

（如果您将两个过程或方法或语句块合并为一个，您会在 Java 中做同样的事情：您需要确保所选变量名称在它们之间是唯一的，这样它们就不会发生冲突。 )

STANDARIZE-APART 正在转换为 CNF，这需要将多个范围合并为一个范围，并消除量词（以及用“and”、“or”等对应物替换某些运算符，例如蕴含和等价运算符, 和“不”)。

存在量词被淘汰，有利于 skolem 函数，如下所示：在二阶（和更高）阶逻辑中，我们可以量化函数（例如 there-exists(f) 使得 f() ...），但是，在 First Order Logic，我们无法量化函数。然而，尽管我们无法量化 FOL 中的函数，但我们仍然可以使用函数。 在 FOL 中，只是假设函数存在。 （CNF 和 horn-clause 形式也尊重假定的函数存在。）Skolemization 是存在量化的替代，其中存在量化的变量（无论它出现在子语句中的何处）被一个新构成的适当参数化的函数替换（为每个这样的存在量词替换组成一个新函数，并且提供的参数与其他封闭量词的上下文有关）。简单地假设这个新引入的函数存在而不需要存在量词。消除了存在量化变量的使用（支持新函数），我们现在可以省略存在量化运算符本身，只保留修改后的子语句。

通用量词被提升到语句的最外层（范围），并且可以简单地消除（1）因为范围已经折叠，（2）因为不再有任何存在量词（因为那些已经被消除了） skolemization) 和 (3) 因为在各种 CNF/horn 形式中，所有变量都被简单地假设为具有普遍量化。

---

统一是一种组合技术，如果我们将关于同一关系 R 的两条（否则分开的）信息组合在一起，我们会考虑我们所知道的内容。这些信息采用关系的变量和常量参数的形式。与标准化不同，统一并不总能成功，也就是说，它并不总是能揭示更多信息。

---

最后一行是对下一级反向链接搜索的反向链接的递归调用，其中已解决的一个目标（例如 CNF 语句）被结果子目标替换。解决我的意思是统一成功，统一成功意味着我们至少名义上提升了搜索引擎的状态，这种进步值得进一步的搜索探索（另一个层次）。