给定一组 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） 为真，则 L2（x） 为真。
所以例如：
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
我想我需要以某种方式"规范化"解析树，然后比较它们。 任何人都可以概述一种方法或草图架构吗？
由于您不对对象（x）执行任何操作，因此您似乎需要命题逻辑，其中p1到pn的真值的所有组合都是可能的。
所以本质上你想在命题逻辑中做定理证明。
您的is_subset(e1,e2)转换为逻辑运算符 e1 implies e2 ，这与 not e1 or e2 相同。要知道这些是否普遍成立，您可以使用满足性检查算法（如 DPLL）检查否定是否不满足。
这只是一个起点，在命题逻辑中还有许多其他选择来证明定理。
您可以将每个公式转换为析取范式，并查找一个公式是否在另一个公式中包含合取子句的子集。这种方法的复杂性随着所提到的 pn 数量的指数而增加。
我认为你的导师本质上希望你实现Quine-McCluskey算法 请注意，正如另一个答案所暗示的那样，执行时间增长得异常快，因为问题是NP困难。