# Existential predecessors Exam 17.02.2016

Exam 17.02.2016

φ= (q1′ ↔ (aq1)) ∧ (q2′ ↔ (q↔ ¬q2)a)

Compute the symbolic representation of the existential predecessors of ¬q∧ q2 How did (q↔¬q2) got changed to (qq2) [ 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

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

+1 vote

There is no practical reason why this conversion was done.

However, it is a quite useful one. Intuitively, it should be quite clear: q↔¬q2 means that q1 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)

by (25.6k points)
selected by
Thank you for the explanation.