# Quantification algorithm

Hi,

I have a doubt regarding the leaf node cases of exists and forall quantification:

forall(leaf, phi)= phi

forall(e, leaf)= leaf

exists(leaf, phi)= phi

exists(e, leaf)= leaf

Can the leaf be 0 and 1 here? Or it's applicable only for if leaf is 1?

Because it's mentioned in the slide number 112 ,

1. 3  Exists(L, φ) = φ (L must be true here),

2. What will happen if L if false?

3.

+1 vote

For the algorithms, forall(e, phi) and exists(e, phi), phi can be an arbitrary BDD, but e is a conjunction of the variables. The recursive calls will either be done with the same BDD e or with its positive cofactor. Hence, it may finally end up with leaf node True, but never with leaf node False.

Moreover, if phi is a leaf node, then the result is phi since the definition of the quantification is the conjunction or disjunction of the cofactors which are however for constants just the constant itself. As we have x&x=x and x|x=x, this is just phi.
by (166k points)
selected by
Yeah..I understood...I couldn't also find any case false as well . Just want to clarify..thanks for the clarification