如何获得命题逻辑中的“间接蕴涵”

Question

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

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

phi => (F => p)

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

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

这里有一个例子，其中“法国”、“里昂”、“巴黎”和“柏林”都是命题：

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）。

再次，我在这里发布它是希望有更多经验的人看到它并说：“啊，但这只是某个问题的变体”。这将是理想的，因为它可以让我利用现有的算法（尤其是可满足性）和概念。

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

感谢您的宝贵时间。

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

因此，要使 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

Answer 2

这是我自己的解决方案。我发布了希望了解标准解决方案的问题，但也许没有。

1. 将F 转换为等价的DNF 公式（析取范式），即连词F1 or ... or Fn 的析取，其中每个Fi 都是一个连词从句。连词从句是文字的连词，其中文字是命题或其否定。将公式转换为 DNF 是一个标准程序。

2. 对于每个分离的Fi。它是以下三种形式之一：

   • L1 and ... and Lmi and p
   • L1 and ... and Lmi and not p
   • L1 and ... and Lmi（p不会出现在里面）。

   设inputs(Fi) 为连词L1 and ... and Lmi，output(Fi) 分别为true、false 和neutral。

   直觉是，如果 Fi 是 F 的 DNF 中唯一的析取词，那么如果 inputs(Fi) 成立，我们需要 p 来获得真值 output(Fi)（neutral 意味着它可以无论哪种方式）让F保持。

3. 当然，问题是Fi 通常不会是唯一的析取词。对于给定的析取 Fi 没有输出 true，可能存在具有不同输出的析取 Fj 使得 ìnputs(Fj) and inputs(Fi) 是可满足的，也就是说，有一个分配给 Fi 的输入满足 @ 987654348@ 也是如此，因此承认p 是假的，同时仍然满足F。 因此，我们将输出命名为trueG1, ..., Gk 和输出为false 或neutralH1, ..., Hl 的分离命名，并将phi 定义为

   （输入（G1）或...或输入（Gk））而不是（输入（H1）或...或输入（Hl））

那么phi 是解决方案，因为它不包含p 并暗示F => p。它不包含p，因为它由inputs 组成，定义为不包含p。它暗示了F => p，因为它至少满足inputs(G_) 之一并且不满足任何inputs(H_)。这意味着，在 F 的 DNF 中的所有析取词中，只有 Gi 有机会成立（除了 p 之外的所有文字都已知满足）。因为它们都包含p，所以如果F 为真，那么p 也一定成立。

让我们看看它如何管理给定的示例。

DNF 的

paris => france and lyon => france and berlin => not france

是

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

因此我们有

• G1 等于 not berlin and france
• H1等于not lyon and not paris and not france

所以

• inputs(G1) = not berlin
• inputs(H1) = not lyon and not paris

因此phi 是

not berlin and not (not lyon and not paris)

相当于

(lyon or paris) and not berlin

解决方案中not berlin 的存在并不直观。它之所以存在是因为F 承认berlin、paris 和lyon 中不止一个同时为真。因此，虽然要求 paris 或 lyon 为真，但它还要求 not berlin，否则将隐含 france 和 not france。在存在说明最多一个变量同时为真的背景知识的情况下，解决方案将是简单的lyon or paris，因为这将自动暗示not berlin。