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

我正在尝试解决命题逻辑中一个我从未见过描述的问题。我将其发布在这里，以查看是否有人对此有一个标准的解决方案。

问题:给定一个命题可满足的逻辑公式F和一个命题p出现在F中，确定是否存在一个不包含 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 or lyon，因为这意味着(F => france)
(更新:实际上精确的解决方案是(paris or lyon) and not berlin，因为我们在任何地方都没有声明这些主张是互斥的，因此paris和berlin(或lyon和berlin)可能同时是真实的，并且存在矛盾。背景知识，该解决方案将简化为paris or lyon)。

它类似于为公式(F => p)找到一个蕴含符的问题，但这并不相同，因为一个简单蕴含符可以包含p(实际上主要蕴含符只是p)。

再次，我将其发布在这里，希望有更多经验的人看着它并说:“啊，但这只是问题之类的一个变种。”那将是理想的，因为它将使我能够利用现有的算法(特别是可满足性)和概念。

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

谢谢你的时间。

最佳答案

给出你的例子

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

因此，要使p中的F为TRUE，您需要满足以下条件才能成为TRUE:

pF1 AND pF2:

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

pF2 = not berlin => berlin = FALSE