algorithm - 如何在命题逻辑中获得一个 "indirect implicant"

Question

我正在尝试解决命题逻辑中的一个问题，我认为我从未在任何地方看到过这个问题。我将它张贴在这里，看看是否有人有一个有希望的标准解决方案。

问题:给定一个命题可满足逻辑公式F和一个出现在F中的命题p，判断是否存在可满足命题公式< strong>phi 不包含 p 这样

phi => (F => p)

如果是，请提供这样的 phi。

出于直觉，我将 phi 称为“p wrt F 的间接蕴涵项”，因为它需要在不提及 p 的情况下蕴涵 p。相反，它提到了通过 F 影响 p 的其他命题。

这是一个例子，其中 'france'、'lyon'、'paris' 和 'berlin' 都是命题:

F is "paris => france and lyon => france and berlin => not france"

p is "france"

然后一个解决方案 phi 是 paris 或 lyon，因为这意味着 (F => france)

(更新:实际上精确的解决方案是(巴黎或里昂)而不是柏林，因为我们没有在任何地方声明这些命题是相互排斥的，所以paris和berlin(或 lyon 和 berlin)可能同时为真并暗示矛盾。在具备适当背景知识的情况下，解决方案将简化为 paris 或 lyon)。

它类似于为公式 (F => p) 寻找蕴涵项的问题，但它并不相同，因为简单蕴涵项可以包含 p(并且事实上，主要蕴含项就是 p)。

再次，我将它张贴在这里，希望有更多经验的人看到它并说:“啊，但这只是问题的变体”。这将是理想的，因为它可以让我利用现有的算法(特别是可满足性)和概念。

此外，只是为了获得更多信息，我实际上是在尝试解决相等逻辑的问题，即命题为等式的命题逻辑。这当然更复杂，但命题案例可能是一个很好的垫脚石。

感谢您的宝贵时间。

Answer 1

举个例子

F is "paris => france and lyon => france and berlin => not france"

p is "france"

F 有 4 个语句:

F1 = paris
F2 = france and lyon
F3 = france and berlin
F4 = not france

F可以分解，通过化简蕴涵=>:

F1-2: "paris => france and lyon" = "(not paris) or (france and lyon)"

F2-3: "france and lyon => france and berlin" = "(not france or not lyon) or (france and berlin)"

F3-4: "france and berlin => not france" = "(not france or not berlin) and (not france)"

如果我们通过 F 推论进行前向链接，我们将进行推理:

Reason(F): not (not (not F1 or F2) or F3) or F4

not (not (not paris or (france and lyon)) or (france and berlin)) or (not france)

所以，我们有以下解决方案:

S1: not france

S2: not (not (not F1 or F2) or F3):
     not (not (not paris or (france and lyon)) or (france and berlin))

接下来我们可以计算p，其中:

p: france => france = TRUE

S1 = not france = not TRUE = FALSE ~ not applicable

S2 = not (not (not paris or (france and lyon)) or (france and berlin))

   = not (not (not paris or (TRUE and lyon)) or (TRUE and berlin))

   = not (not (not paris or lyon) or berlin)

   = not ((paris AND not lyon) or berlin)

   = not (paris AND not lyon) AND not berlin

   = not (paris AND not lyon) AND not berlin

   = (not paris OR lyon) AND not berlin

因此，要使 F 中的 p 为真，您需要这些条件为 TRUE:

pF1 AND pF2:

pF1 = (not paris OR lyon) = (paris,lyon) in { (F,F), (F,T), (T,T) }

pF2 = not berlin => berlin = FALSE