时间戳

首页 > 解决方案 > 在没有指数爆炸的情况下将一阶逻辑转换为 CNF

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

问题描述

当试图在计算机上解决逻辑问题时，通常首先将它们转换为 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？

标签： first-order-logicconjunctive-normal-form

解决方案

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

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

  • 将诸如 ∃Xp(X) 之类的存在主义转换为诸如 ¬∀Yp(Y) 之类的全称，反之亦然，因此你有一个规范形式。在稍后的步骤中进行 Skolemize。
  • 请记住，当你转换你的 p(S) 是一个 Skolemized 存在时，它的否定是 ∀Y.¬p(Y)。
  • 定义等价于全称和存在的术语，使得 a 表示 ∀Yp(Y) 并且 ¬a 然后表示 ¬∀Yp(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) 转换所追求的。

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

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

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

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

推荐阅读