Question

linear-size clause form:

a → (b ∨ ¬(c ∧ d))

Solution:

x0 <-> (c∧d) : {x0,¬c,¬d}{¬x0,c}{¬x0,d}

x1 <-> ¬x0    : {x1,x0}{¬x0,¬x1}

x2 <-> (b∨x1) : {b,x1,¬x2}{x2,¬b}{x2,¬x1}

*** x3 <-> (a→x2)  : {x3,¬a}{x3,x2}{a,¬x2,¬x3} 

x3: {x3}

for part (***) I have transformed to clause by below:

x3 <-> (a→x2)

=> (x3 → (a→x2)) ∧ ((a→x2) → x3)

=> (x3 → (a∨¬x2)) ∧ ((a∨¬x2) → x3)

=> (x3 ∨ ¬(a∨¬x2)) ∧ ((a∨¬x2) ∨¬x3)

=> (x3 ∨ (¬a∧x2)) ∧ ((a∨¬x2) ∨¬x3)

=> (x3 ∨ ¬a)∧(x3 ∨ x2)∧(a∨¬x2∨¬x3)

BUT, when I compare it with teaching tool result they are different.

Please may clarify which part I have done wrongly?

Thank you.

Answer 1

You have some errors in the transformations. Note that (a→b) is equivalent to ¬a∨b and not a∨¬b (which you have used). Then the conversion to clause form of x3 <-> (a→x2) is as follows:

x3 <-> (a→x2)
<=> (x3 → (a→x2)) ∧ ((a→x2) → x3)
<=> (x3 → (¬a∨x2)) ∧ ((¬a∨x2) → x3)
<=> (¬x3 ∨ (¬a∨x2)) ∧ (¬(¬a∨x2) ∨ x3)
<=> (¬a∨x2∨¬x3) ∧ (a∧¬x2 ∨ x3)
<=> (¬a∨x2∨¬x3) ∧ (a∨x3) ∧ (¬x2∨x3)

Comments

Thank you for clarification.