Symbolic representation of kripke structure

Question

I have some doubt regarding the finding the set of existential or universal successor or predecessor finding using symbolically.

Suppose at the end after substituting next(p) and next(q) we get the proposition formula like [((p  or q ) <->  q ) & !(q <-> (( p or q) <-> q) )] . And the question is like to give the ans in DNF. So can I use the truth table to get the SOP(sum of product). Like for this if i try to substitute the p and q value I get !p&!q. Or is there any other alternative approach to find the DNF??

Answer 1

There are many ways to convert a propositional logic formula into a DNF, one of them is the use of the truth table which is however typically the worst effort. My recommendation would be to use the Shannon decomposition, i.e., make a case distinction on the variable p, and you will quickly see that the formula is equivalent to !p&!q.