逻辑表达式的联合算法？(Algorithm For Intesection of Logical Expressions?)

逻辑表达式的联合算法？(Algorithm For Intesection of Logical Expressions?)

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

我认为我需要以某种方式“正常化”解析树，然后进行比较。 任何人都可以勾画出一种方法或勾画出一种架构吗

Given a set of n elements U, and a set of m properties P where each element of P defines a function from U to boolean.

Given two composite logical expressions of the form (recursively defined):

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

These logical expressions are parsed into expression statements (parse trees).

Assume that for any p1, p2: All four sets (p1 and p2), (p1 and not p2), (not p1 and p2), (not p1 and not p2), are non-empty.

I want to determine if a logical expression L1 is a subset of L2. That is for every element x in U, if L1(x) is true then L2(x) is true.

So for example:

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

I think I need to "normalize" the parse trees somehow and then compare them. Can anyone outline an approach or sketch an architecture?

最满意答案

既然你没有对对象（x）做任何事情，似乎你想要命题逻辑，其中p1到pn的真值的所有组合都是可能的。

所以基本上你想在命题逻辑中做定理证明。

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

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

Since you don't do anything with the objects (x) it seems you want propositional logic, where all combinations of the truth values for p1 to pn are possible.

So essentially you want to do theorem proving in propositional logic.

Your is_subset(e1,e2) translates to a logical operator e1 implies e2, which is the same as not e1 or e2. To know if these hold universally you can check if the negation is unsatisfiable with an algorithm for satisfiability checking such as DPLL.

This is just a starting point, there are many other options to prove theorems in propositional logic.