What would be the ZDD approach in Prolog that also provides quantifiers.
Notation for existential quantifier would be as follows:
where X is the bound variable and F is the formula. It corresponds
to the following formula:
F[X/0] v F[X/1]
How would one go about and write a Prolog routine that takes a ZDD
for F and a variable X and produces the ZDD for X^F ?
P.S.: Cross posted on stackoverflow. https://\stackoverflow.com/q/64959919/502187
But I am not sure whether Kuniaki Mukai visits stackoverflow.