Result is incorrect though it satisfies CNF

Question

In problem 3 for the following given equation resulted solution which satisfies CNF definition.

x <-> (y1 & y2)

[x -> (y1 & y2)] & [(y1 & y2) -> x]

[ !x | (y1 & y2) ] & [ !(y1 & y2) | x ]

(~x | y1) & (~x | y2) & (!y1 | !y2 | x)

But the system shows it as incorrect. What should be modified in this case? Isn't it satisfies CNF definition?

Update: actually submitted (!x | y1) & (!x | y2) & (x | !y1 | !y2)

Answer 1

Let's go through it step by step:

x ↔ (y1 ∧ y2) // the formula
[x →(y1 ∧ y2) ] ∧ [(y1 ∧ y2) → x] // display ↔ as a conjunction of two implications
[¬x ∨ (y1 ∧ y2) ] ∧ [¬(y1 ∧ y2) ∨ x] // remove the implication syntactic sugar
(¬x ∨ y1) ∧ (¬x ∨ y2) ∧ (¬y1 ∨ ¬y2 ∨ x) // multiply out (left), apply de-morgan (right)

So your formula does make sense to me.

Make sure that you don't confuse ^/⊕/xor for &/∧/and as shown here: https://q2a.cs.uni-kl.de/469/exercise-sheet-1-task-3-e-broken

Answer 2

Your computations are correct, but you are not consistent with your syntax, and I guess that is your problem. Replace "~" with "!" and the delimiters "[", "]" with "(", ")" and then it should be fine.

Comments

The shown syntax was not the one entered for exercise submission. If one submits the last line in the original question, the result is:
“Details: ERROR: parse error : (~x | y1) & (~x | y2) & (!y1 | !y2 | x) Logic expression parsing failed. The following example shows valid syntax: a & b | c ^ (a -> e) | (a?true:c)”
For this task, the system only marks syntactically right but semantically wrong answers as “incorrect”. The problem is just that the student read ^ as &/∧/and although it should be  ^/⊕/xor.

---

Okay, so another problem was solved correctly with typos. Understood!

---

I submitted in this form (!x | y1) & (!x | y2) & (x | !y1 | !y2)
But while typing the question I mixed up the signs.
Now the task displayed as x ↔ (y1 ⊕ y2).

---

Yes. I saw that some students were misreading the xor ^ as the conjunction ∧. So I changed the task so that it gives a hint which connectives mean the same, and that the tasks are displayed in Unicode™.

---

Last question regarding solving negation of xor. Let we resolve the following:
!(y1 xor y2) | x
= ![ (y1 & y2) | (!y1 & !y2) ] | x // xor simplification
= [ (!y1 | !y2) & (y1 | y2) ] | x // de-morgan's law
= ( x | !y1 | !y2 ) & (x | y1 | y2) // distribution of or over and

which is incorrect. I verified both in ES Proposition Logic tool and WolframAlpha tool that (x | !y1 | y2) & (x | y1 | !y2) is correct but I could not understand.

UPDATE: Understood, I made mistake in xor simplification, it should be (y1 & !y2) | (!y1 & y2)

---

The negation in the first step was wrong. You replaced xor by a formula expression equality. That's already the negation of xor, so the outer negation sign should disappear.