Let's say you name your function CNF
, taking a tree and returning the tree in CNF.
First, replace equivalency
p<=>q
withAND(p=>q,q=>p)
then replace implicationsp=>q
withOR(q,NOT(p))
.Convert to negation normal form: move all
NOT
operations down the tree, so that theNOT
operations bind only to atoms (A
,B
).Then, the result of
CNF(AND(x,y))
is simple:AND(CNF(x),CNF(y))
, as it is CNF-like to haveAND
s high in the tree.The result of
CNF(OR(AND(x,y),z))
is a little bit more complicated. Here we will use the rule of distribution of disjunction over conjunction, which isOR(AND(x,y),z)
is equivalent toAND(OR(x,z),OR(y,z))
. In effect,CNF(OR(AND(x,y),z))
will beAND(OR(CNF(x),CNF(z)),OR(CNF(y),CNF(z))
.
And you're done.