first-order-logic - 将一阶逻辑转换为 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)。

使用 bool 对偶的对称性，以便相同的变换适用于 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。量词变换的内部 ¬ 和德摩根变换的外部 ¬ 相互抵消。最后，当您将每个 ∨ 和 ∧ 替换为另一个并且将任何原子 a 或 ¬a 替换为其逆时，任何 bool 等价的对偶仍然有效。

因此，虽然我可能会犯错误，尤其是在凌晨 1 点，但在我看来，您想要的是替代的双重转换:

∀ 的外部 ∃ 反之亦然

∧ 代表 ∨ 反之亦然

每个术语 t 与 ¬t 反之亦然

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