Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

928 questions

1k answers


441 users

0 votes

Based on the solutions of exams 19.02.2020 and 20.08.2020, I have understood that we can make cuts in BDD based on the variables to quantify on. So, I am wondering if similar rule can be applied for ForAll as well. The following illustrates it in more detail.

in * TF "Emb. Sys. and Rob." by (480 points)
edited by

1 Answer

+1 vote
Best answer
Yes, you can do that since the Forall algorithm is just a dual to the Exists algorithm. That means if you would compute the Forall operation as negation of Exists of the negation, you would to the same cut as well. The difference is just that you have to compute a conjunction instead of the disjunction, as you know.
by (143k points)
selected by

Related questions

0 votes
1 answer
0 votes
1 answer
0 votes
1 answer
Imprint | Privacy Policy