MGU和可变标准化-CNF

Question

我一直在阅读将一阶逻辑句子转换为结合词法形式，然后执行分辨率。

转换为CNF的步骤之一是标准化变量：重命名所有变量，以使每个量词都具有自己的独特变量名称。

大多数一般的统一是两个条款的最不专业统一。

问题1：我一直在寻找一个示例，该示例表明如果我不标准化变量，那么我发现的所有在线资源都只能解释“如何”而不是“为什么”。您能为我提供一个潜在问题的例子吗？

问题2：与第一个问题相同的问题。如果我们不使用MGU并使用更专业的Unifier怎么办？有什么潜在问题？你能为我提供一个例子吗？

我真诚的谢谢。费利佩

Answer 1

1. 看 这个答案 - 这是一组矛盾的子句的一个示例，我们不能在不重命名变量的情况下得出矛盾。请注意，转换为CNF后仅重命名变量是不够的，我们必须将变量重命名为不同 每一个 解决方案规则的应用。您可以将其视为如下：在两个不同的子句中出现的变量在每个子句中都具有不同的含义，因为它们隐含地被普遍量化。如果我们不在其中一个子句中重命名变量，我们会做出一个错误的假设，即在两个子句中均表示相同。

2. 通过使用MGU，我们在分辨率步骤中得出最通用的子句。如果我们使用比其MGU更专业的统一器，则结果条款较弱。这意味着我们没有推断出所有的知识，即使存在，我们也会错过一个空句的推论。例如： begin {array} {c} p（x，y） lor q（y） lnot q（d） lnot p（c，d）使用MGU从前两个条款分解，将$ y 发送到D $，我们得到$ P（x，d）$，我们可以继续使用第三子句。如果我们采用较弱的统一器，例如也将$ x 发送到d $的统一器，我们将获得$ p（d，d）$，并且我们无法与第三子句解析。这意味着该方法不再完成。