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