An algorithm for injecting logical expressions?

Question

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

Given two composite logical form expressions (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 in expressions (parsing trees).

Suppose that for any p1, p2: all four sets (p1 and p2), (p1 and not p2), (not p1 and p2), (not p1, not p2) are nonempty.

I want to determine if the logical expression L1 is a subset of L2. That is, for each element x from 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 somehow "normalize" the parsing trees, and then compare them. Can someone outline an approach or sketch of architecture?

Answer 1

Since you are not doing anything with objects (x), it seems that you need propositional logic where all combinations of truth values ​​from p1 to pn possible.

So, you essentially want to prove the theorem in propositional logic.

Your is_subset(e1,e2) translates to the logical operator e1 implies e2 , which is the same as not e1 or e2 . To find out if they are universal, you can check if a validation algorithm such as DPLL negates the negation.

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

Answer 2

You can convert each formula into a disjunctive normal form and find if it contains a subset of conjunctive sentences in another. The complexity of this approach increases as an indicator of the number of pn mentioned.

Answer 3

I think that your instructor essentially wants you to implement Quine-McCluskey Algorithm. Please note that, as another answer suggests, the execution time grows extremely fast because the problem is NP Hard.