# Convert propositional logic to CNF

Q: a<->(b->d)&a<->(c->d)&d&c|!(d&d)

Steps I've tried:

d&c|!(d&d) -> (c&!d)

Using SNF:

1.) a<->(b->d) -> (a|b&!d) & (!a|!b|d)

2.) a<->(c->d) -> (a|c&!d) & (!a|!c|d)

(a|b&!d)&(!a|!b|d)&(a|c&!d)&(!a|!c|d)&(c&!d)

I notice that the formula of the accepted answer exists in my last stage but I cannot figure out what further simplifications can I proceed with.

d&c|!(d&d) is not a subformula of your formula, note that conjunction binds stronger than disjunction.

+1 vote

Why not proceeding this way (using Shannon decomposition)?

Note that we have (x⇒φ|ψ) ⇔ (¬x ∨ φ) ∧ (x ∨ ψ)

a<->(b->d)&a<->(c->d)&d&c|!(d&d)

<=> (¬d ∨ (a<->(b->1)&a<->(c->1)&1&c|!(1&1))) ∧ (d ∨ (a<->(b->0)&a<->(c->0)&0&c|!(0&0)))

<=> (¬d ∨ (a<->a<->c)) ∧ (d ∨ (a<->(!b)&a))

<=> (¬d ∨ c) ∧ (d ∨ (a<->!b&a))

<=> (¬d ∨ c) ∧ (d ∨ (¬a ∨ (1<->!b&1)) ∧ (a ∨ (0<->!b&0)))

<=> (¬d ∨ c) ∧ (d ∨ (¬a ∨ !b) ∧ (a ∨ 1))

<=> (¬d ∨ c) ∧ (d ∨ (¬a ∨ !b) )

<=> (¬d ∨ c) ∧ (d ∨ ¬a ∨ !b )
by (143k points)
selected by
It didn't occur to me to try Shannon Decomp from the get go. That's why I tried to simplify first. It's clear now.