在没有指数爆炸的情况下将一阶逻辑转换为 CNF

Question

当试图解决计算机上的逻辑问题时，通常首先将它们转换为 CNF，因为最好的解决算法期望 CNF 作为输入。

对于命题逻辑，这种转换的教科书规则很简单，但如果你照原样应用它们，结果是程序遇到双指数资源消耗而不被专门为此设计的：

a <=> (b <=> (c <=> ...))

使用 N 个变量，生成 2^2^N 个子句，一个指数级爆炸将等价转换为 AND/OR，另一个将 OR 分配为 AND。

解决方案是重命名子项。如果我们将上面的内容重写为类似

r <=> (c <=> ...)
a <=> (b <=> r)

其中r 是一个新符号，被定义为等于子项 - 通常，我们可能需要 O(N) 个这样的符号 - 可以避免指数爆炸。

不幸的是，当我们尝试将其扩展到一阶逻辑时遇到了问题。使用 TPTP 表示法，其中? 表示“存在”并且变量以大写字母开头，考虑

a <=> ?[X]:p(X)

诚然，这种情况很简单，实际上不需要重命名子项，但有必要使用一个简单的情况来说明，所以假设我们使用的算法只是自动重命名等价运算符的参数；这一点可以推广到更复杂的情况。

如果我们尝试上述技巧并重命名? 子项，我们会得到

r <=> ?[X]:p(X)

存在变量被转换为 Skolem 符号，因此最终为

r <=> p(s)

原来的公式然后展开为

(~a | r) & (a | ~r)

构造上等同于

(~a | p(s)) & (a | ~p(s))

但这是不正确的！假设我们没有进行重命名，只是将原来的公式扩展为原来的样子，我们会得到

(~a | ?[X]:p(X)) & (a | ~?[X]:p(X))
(~a | ?[X]:p(X)) & (a | ![X]:~p(X))
(~a | p(s)) & (a | ~p(X))

这与我们通过重命名获得的版本截然不同。

问题是等价需要每个论点的正面和负面版本，但是将否定应用于包含全称或存在量词的术语，会在结构上改变这些术语；您不能只将它们封装在定义中，然后将否定应用于定义的符号。

这样做的结果是，当您有等价并且参数可能包含此类量词时，您实际上需要重复每个参数两次，一次用于肯定版本，一次用于否定版本。这足以带回我们希望通过重命名来避免的存在性爆炸。据我所知，这个问题不是由特定算法的工作方式引起的，而是由任务的性质引起的。

所以我的问题：

给定一个可能包含等价和量词的任意嵌套的输入公式，是否有任何算法可以正确地将其转换为具有多项式而不是指数子句数的 CNF？

Answer 1

正如您所观察到的，诸如 ∃X.p(X) 之类的存在式实际上 不 等价于 Skolemized 表达式 p(S)。它的否定¬∃X.p(X)不等价于¬p(S)，而是等价于∀Y.¬p(Y)。

避免指数爆炸的可能方法：

• 将诸如 ∃X.p(X) 之类的存在式转换为诸如 ¬∀Y.p(Y) 之类的全称，反之亦然，这样您就有了一个规范形式。在稍后的步骤中进行 Skolemize。
• 请记住，当您转换 p(S) 是一个 Skolemized 存在时，它的否定是 ∀Y.¬p(Y)。
• 定义等价于全称和存在的术语，例如 a 表示 ∀Y.p(Y) 并且 ¬a 然后表示 ¬∀Y.p(Y)，或者等效地，∃X.¬p(X)。
• 使用布尔对偶的对称性，以便相同的转换适用于 AND 和 OR 交换、德摩根定律以及存在主义和否定普遍性之间的等价性，以恢复 r 和 ~r 的展开之间的对称性。普遍性和存在性转换中的否定和德摩根定律中的否定相互抵消，并且切换AND和OR的二元性意味着您可以重复使用左侧的结果再次机械地生成右侧的结果？李>

鉴于您无论如何都需要支持ALL 和NOT ALL 语句，这不会产生任何新问题。只需规范化并使用与通用方法相同的方法即可。

如果您通过转换为 SAT 来解决问题，那么您的术语也可以代表普遍性。因此，在您的示例中，您尝试将 a 替换为 r，但您仍然可以使用 ~a，相当于否定通用。

在你的表达中。您仍然会使用 (~a | r) & (a | ~r)，但将 ~r 扩展为正确的值而不是错误的值。这个例子很简单，因为它只是~a，但您通常会将r 定义为等价于更复杂的转换，在这种情况下，您需要记住r 和~r 代表什么。这并不是 Skolemized 表达式的简单机械转换。

在这个例子中，我不知道为什么(~a | r) & (a | ~r) 等同于(~a | r) & (a | ~a) 是一个问题，它简化为(~a | r)。这不会给你带来指数级的爆炸吗？当您转换回一阶谓词逻辑时，请进行正确的转换。

更新

感谢您澄清聊天中的问题所在。正如我目前认为我理解的那样，您所拥有的是具有左右两侧的等价，其中包含其他嵌套的等价，并且您想要扩展等价及其否定。问题是，因为否定没有对称形式，所以对于树中的每个嵌套等价，都需要递归两次，一次是展开等价，一次是展开它的否定？

您应该定义一个在线性时间内从正扩展生成负扩展的转换，并使用它来分治包含嵌套等价的表达式。这似乎是您使用 ~p(S) 转换所追求的。

为此，您还记得 ¬∃X.p(X) 等价于 ∀X.¬p(X)，反之亦然。然后，如果您将 p(x) 扩展为合取和析取的正规形式，德摩根定律允许您将 ¬(a ∨ ¬b) 之类的表达式转换为 ¬a ∧ b。量词变换的内部 ¬ 和 De Morgan 变换的外部 ¬ 相互抵消。最后，当您将每个 ∨ 和 ∧ 替换为另一个并且将任何原子 a 或 ¬a 替换为其逆时，任何布尔等价的对偶仍然有效。

所以，虽然我可能会出错，尤其是在凌晨 1 点，但在我看来，您想要的是替代的双重转换：

• ∀ 的外部∃，反之亦然
• ∧ 表示 ∨，反之亦然
• 每个术语 t 和 ¬t 反之亦然

将此应用于正等价的展开，以在时间上与其长度成正比生成负对偶，无需进一步递归。