逻辑表达式相交的算法？

Question

给定一个由 n 个元素 U 组成的集合，以及一组包含 m 个属性 P 的集合，其中 P 的每个元素都定义了从 U 到布尔值的函数。

给定两个形式为（递归定义）的复合逻辑表达式：

p1 : true iff p1(x) is true
e1 and e2 : means e1 and e2 are both true
e1 or e2 : means e1 and e2 are not both false
not e1 : true iff e1 is false
(e1) : true iff e1

这些逻辑表达式被解析为表达式语句（解析树）。

假设对于任意p1、p2：四个集合（p1和p2）、（p1且非p2）、（非p1且p2）、（非p1且非p2）都是非空的。

我想确定逻辑表达式L1是否是L2的子集。也就是说，对于U中的每个元素x，如果L1(x)为true，则L2(x)也为true。

例如：

is_subset(not not p1, p1) is true
is_subset(p1, p2) is false
is_subset(p1 and p2 and p3, (p1 and p2) or p3) is true

我认为我需要以某种方式“规范化”解析树，然后进行比较。是否有人能够概述一种方法或勾勒出一个架构？

- Andrew Tomazos

---

抱歉，这与你的问题无关，但我想知道：你会推荐哪种编程语言用于形式逻辑编程？ - QuietThud

@QuietThud: Prolog是最常见的逻辑教学语言。在这个领域中，我们借鉴逻辑编程语言中学到的“模式”，但将它们作为库特性实现在像C++这样的工业语言中。 - Andrew Tomazos

@AndrewTomazos-Fathomling：我觉得可能有一种类似于统一的解决这个问题的方法，但可能需要一些调整。想提一下以防万一。 - Asiri Rathnayake

不，你不需要统一，因为对象x没有任何结构，它们没有被使用。 - starblue

Answer 1

由于您不对对象（x）进行任何操作，因此似乎您想要命题逻辑，其中可能存在 p1 到 pn 的所有真值组合。

因此，您基本上想在命题逻辑中进行定理证明。

您的 is_subset(e1,e2) 转换为逻辑运算符 e1 implies e2，它与 not e1 or e2 相同。要知道这些是否普遍成立，可以使用可满足性检查算法（例如 DPLL）检查否定是否不可满足。

这只是一个起点，在命题逻辑中证明定理还有许多其他选项。

- starblue

---

这是一个有趣的想法。我可以将L3合成为(not (L1)) and (L2)，然后确定L3是否为空。我需要在L3上搜索像X and not X -> false和X and X -> X这样的转换，以尝试使其解析为false。 - Andrew Tomazos

Answer 2

你可以将每个公式转换为析取范式，并查找是否存在一个公式包含另一个公式中的合取子句的子集。这种方法的复杂度随着pn数量的指数级增长。

- Alexey Feldgendler

Answer 3

我认为你的教练基本上希望你实现Quine-McCluskey算法。请注意，正如其他答案所暗示的那样，执行时间增长得非常快，因为这个问题是NP难题。

- SAJ14SAJ