逻辑表达式的交集算法？答案

【问题标题】：Algorithm For Intesection of Logical Expressions?逻辑表达式的交集算法？
【发布时间】：2012-11-13 11:00:19
【问题描述】：

给定一组 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

我认为我需要以某种方式“规范化”解析树，然后比较它们。任何人都可以概述一种方法或勾勒出架构吗？

【问题讨论】：

对不起，这与你的问题无关，但我想知道：你会推荐什么语言来编程形式逻辑？
@QuietThud：Prolog 是最常见的逻辑教学语言。在该领域中，我们借用从逻辑编程语言中学习到的逻辑编程“模式”，但将它们实现为工业语言（如 C++）中的库功能。
@AndrewTomazos-Fathomling：我觉得使用类似于Unification 的方法可能会解决这个问题，但可能需要一些修补。为了以防万一，想指出来。
不，你不需要统一，因为对象x没有任何结构，它们不会以任何方式使用。

标签： algorithm math logic boolean-logic

【解决方案1】：

由于您不对对象 (x) 做任何事情，因此您似乎需要命题逻辑，其中p1 到 pn 的真值的所有组合都是可能的。

所以本质上你想在命题逻辑中进行定理证明。

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

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

【讨论】：

这是一个有趣的想法。我可以将L3合成为(not (L1)) and (L2)，然后判断L3是否为空。我必须在 L3 上搜索 X and not X -> false 和 X and X -> X 之类的转换，以尝试使其解析为 false。

【解决方案2】：

您可以将每个公式转换为disjunctive normal form 并查找其中一个是否包含另一个中的连接子句的子集。这种方法的复杂性随着提到的 pn 数量的指数而增加。

【讨论】：

【解决方案3】：

我认为您的讲师本质上是希望您实现Quine-McCluskey Algorithm 请注意，正如另一个答案所暗示的那样，执行时间增长得非常快，因为问题是-NP Hard。

【讨论】：