What would be the ZDD approach in Prolog that also provides quantifiers.
Notation for existential quantifier would be as follows:
X^F
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.
I have not any answer to the point for your question. I am still enjoying debugging in my codes on ZDD to count paths in directoed graphs. However, as in the demo CGI, being inspired by a ZDD article (in Japanese), ZDD could be viewed as a system of polynomials with a familiar set of operations. (Also a member of this forum kindly sent to me a URL on Knuth’s lecture video on ZDD, which seems about algebras on ZDD, though I have not yet wached. ) Anyway if your question is related on polynomials in some way, also I will consider it in the future. But for now, I am in the mode “debug first.”