existential predecessors

Question

Can some one please help me with below problem :

Compute the existential predecessors of the state set specified by the propositional logic formula p ∧ ¬q symbolically. Perform the computation on the corresponding Kripke structure. Convert your result to a quantifier-free formula in DNF (recall: ϕR = a ∧ ((p ∧ q) ↔ ¬p 0 ) ∧ (q 0 ↔ (¬p ∧ ¬q))).

Answer 1

I don't see where exactly your problem is. I can tell you the general prodecure:

• There is a formula for existential predecessors in the lecture notes. Slide 58-59, followed by examples
• Plug the set and the relation to the formula
• Do the renaming (here it's changing the formula specifying the set from p ∧ ¬q to p' ∧ ¬q')
• Unfold the quantification. Let the exists operator become a disjunction of copies of the inner formula where all possible truth values for the quantified variables are plugged in
• Simplify the formula

The questions looks like an exam question. Maybe you can look at the standard solution to learn from that after trying it on your own.