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

Question

我能解释一下for each循环吗，因为它对我来说没什么意义。特别地，标准化Apple（）和第二条最后一行是什么？
即FOL_BC_ASK(KB,[p1...,pn|REST(goals)],COMPOSE(@',@)) U ans

Answer 1

r是知识库中的fol语句。
除其他外，fol语句可以包含量词和变量。
对于任何fol语句，它都有一个简化的形式，有多种形式，如cnf（连接范式）（horn子句是相似的），该算法对其进行操作。cnf风格的简化仅限于特定的、有限的运算符集，并且通常会导致与原始语句相比的扩展语句（有时长得多）。cnf不使用量词，但允许使用变量。
量词是“为所有”（万有）和“存在”（存在）的运算符。每个量词都有一个变量（或变量列表）和一个单独的（子）语句，在这个语句中引入的变量（在列表中）被量化。这些变量被称为是有界的，尽管只是一个子语句的范围（在量化表达式中）。因此，量词隐式地引入了一个新的作用域（用于其变量）。
cnf不允许显式表示的量词，也不为变量提供多个或单独的作用域！因此，不仅必须删除量词，还必须删除变量的作用域（或折叠为单个作用域）。（范围很容易消除，所以这是首先完成的。）
当一条语句包含多个量词时，在fol中完全可以接受在具有不相交范围的量词中重用相同的变量名。因此，以下单语句（尽管是复合语句）在下文中是可接受的：

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

也就是说有些X是乔的父亲，有些X（另一个X）是乔的母亲。
在上面的语句中，变量x被引入了两次，尽管它的两个不同用法实际上是不相关的！但是，由于x被使用了两次，当我们读取、解释或操作并转换此语句时，我们必须保持对这两个独立作用域的了解（否则，我们的转换有时将无法等效）。这在任何fol语句中都是正确的，这意味着我们需要了解范围界定，以便对一般fol语句进行解释和操作。
从逻辑角度看，以下语句是等效的，但不使用x两次：

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

如果我们保证（转换的）语句没有重叠的变量（即在不相交的作用域中不存在同一变量名的两个用法），我们就不再需要考虑量化的两个用法引入的两个独立作用域。我们可以有效地考虑这样的语句的变量只有一个作用域。这是标准化隔离的本质，通过确保范围内的变量不重叠（通过赋予它们每个唯一的名称），我们不再需要在单个语句（可能有多个量词）中单独考虑多个范围。
（如果将两个过程、方法或语句块合并为一个过程、方法或语句块，则在Java中也会执行相同的操作：要确保所选的变量名在它们之间是唯一的，这样它们就不会冲突。）
标准化分离是对CNF的转换，它需要将多个范围折叠成一个，并且消除量词（以及替换某些运算符，如含义和等价性），以“和”、“或”和“不”为条件。
存在的量词被排除在SKOLEM函数的下面：在第二（和更高）阶逻辑中，我们可以对函数进行量化（例如存在（f），使得f-（…）…），然而，在一阶逻辑中，我们不能对函数进行量化。尽管我们不能量化fol中的函数，但我们仍然可以使用函数。在FOL中，函数简单地假定存在。（CNF和HONN子句形式也尊重函数的假定存在）。SkoLeM化是对存在量化的替换，其中存在的量化变量（在子语句中出现的任何地方）用新的适当的参数化函数来代替（每个函数都是新的函数）。存在量词替换，所提供的参数与其他封闭量词的上下文有关。这种新引入的函数简单地假设存在而不需要存在量词。消除了存在量化变量的使用（有利于新函数），现在我们可以省略存在量化算子本身，只保留修改后的子语句。
通用量词被提升到语句的最外层（作用域），并且可以简单地删除（1）因为作用域已经折叠，和（2）因为不再存在任何存在量词（如已经被SkeleMe化消除）和（3），因为在各种CNF/HORM形式中，所有变量都简单地假设具有通用量化。
统一是一种组合技术，在这种组合技术中，如果我们将关于同一关系的两条（或两条）信息r组合在一起，我们就会考虑我们所知道的内容。这些信息的形式是关系的变量和常数参数。与标准化不同，统一并不总是成功的，也就是说，它并不总是揭示更多的信息。
最后一行是为下一级反向链接搜索递归调用反向链接，其中已寻址的一个目标（例如cnf语句）被结果子目标替换。我所说的地址是指统一成功，统一成功意味着我们至少在名义上提升了搜索引擎的状态，这一进步值得进一步的搜索探索（另一个层次）。