Existential predecessors Exam 17.02.2016

Question

Exam 17.02.2016

φR = (q1′ ↔ (a⊕q1)) ∧ (q2′ ↔ (q1 ↔ ¬q2)∧a)

Compute the symbolic representation of the existential predecessors of ¬q1 ∧ q2

How did (q1 ↔¬q2) got changed to (q1 ⊕q2) [ highlighted in the green color ]

I know 

1. (a ⊕ b) = ¬ (a ↔ b) = (a ∧ ¬b) v (¬a ∧ b) = (a v b) ∧ (¬a v ¬b)

2. 1 ↔ a = a

Can someone please explain?

link to the question paper (Question 4 (b)): https://es.cs.uni-kl.de/teaching/vrs/exams/2016.02.17.vrs/2016.02.17.vrs.solutions.pdf

Answer 1

There is no practical reason why this conversion was done.

However, it is a quite useful one. Intuitively, it should be quite clear: q1 ↔¬q2 means that q₁ and ¬q2 must have the same value. As one of them is negated, this is the same as the values need to be different. That's exactly what xor checks.

By the way: Your first line of equations is already a good start. Let's not negate the xor though:

(a ⊕ b) = a∧¬b ∨ ¬a∧b = a∧(¬b) ∨ ¬a∧¬(¬b)

This looks pretty much like the DNF-Version of biimplication, doesn't it? Just that the right operand is ¬b:

= (a↔¬b)

Comments

Thank you for the explanation.