# Check if one condition includes another

I have two conditions A and B in a form of "ast tree". How can I check that B is more strict than A? I.e. if B is true then A is always true.

Example

A: x = 1 and (b = 2 or c = d)

B: y = 5 and x = 1 and (b = 2 or c = d)

Does B include A -> true

A: x = 1 and (b = 2 or c = d)

B: y = 5 and x = 1 and (b = 2 or c = d)

Does B include A -> false

This seems to be a common task for a specialist in logical math. But I have only very basic knowledge about logical arithmetics. Any articles/studies about subject appreciated.

• An approach might be modelling $A$ and $B$ in a model checker and then verifying if the formula $B \to A$ is tautological. That being said, this is probably way too complex for someone with "only very basic knowledge about logical arithmetics"... Dec 31 '18 at 10:44
• What form can the conditions take? Without more information, your question can't really be answered: for example, if the only condition that's allowed is "true", then the problem is trivial; if you're allowed conditions such as "If Turing machine $M$ halts on input $x$", then the problem is undecidable. Dec 31 '18 at 21:49

If your ASTs have a small number of conditions, then you can use the following naive approach.

1) Convert your ASTs to a CSOP (Canonical Sum Of Products) expression. From your example, lets convert each condition to a boolean variable and express $$A$$ and $$B$$ as boolean expressions in the following variables

$$p: (x ==1)$$
$$q: (y==5)$$
$$r: (b == 2)$$
$$s: (c == d)$$

Now
$$A: \space p \cdot (r + s)$$
$$B: p \cdot q \cdot (r + s)$$

Normalising $$A$$ and $$B$$ yields
$$A: p \cdot \lnot q \cdot r \cdot \lnot s + p \cdot \lnot q \cdot r \cdot s + p \cdot q \cdot r \cdot \lnot s + p \cdot q \cdot r \cdot s + p \cdot \lnot q \cdot \lnot r \cdot s + p \cdot q \cdot \lnot r \cdot s$$
$$B: p \cdot q \cdot r \cdot \lnot s + p \cdot q \cdot \lnot r \cdot s + p \cdot q \cdot r \cdot s$$

2) Check if $$B \subseteq A$$. In the above example it is true. This implies $$B$$ is stricter than $$A$$. If thought logically, all conditions in $$B$$ are fulfilled by $$A$$, but $$A$$ also satisfies other conditions not in $$B$$. Hence, $$B$$ is stricter compared to $$A$$.

Note: Expanding boolean expressions to normal forms requires exponential space. The algorithm might need some optimisation tweaks for larger expressions.

• Your answer guided me to the right solution - thank you. But I thinking convering to Canonical Product of Sum instead, and after that's done - checking if all terms of one expressions are found in another. Else I don't see a way to "Check if B⊆A" in CSOP. Dec 31 '18 at 22:20
• @YuriYaryshev Yes. Even CPOS can be used for the task. But use the correct one based on the expression. If an expression has $n$ variables (4 in the example) and the CSOP has $x$ product terms, then CPOS will contain $2^n-x$ sum terms. So choosing the correct Canonical form can reduce the runtime of the algorithm. Jan 1 '19 at 4:14