CIS 301. Computing a negation normal form.
function NNF(phi)
precondition: phi is implication free with generating gammar
phi ::= p | phi | phi phi | phi phi
postcondition: NNF(phi) computes a nnf for phi
begin function
case
phi is a literal : return phi
phi is phi1 : return NNF(phi1)
phi is (phi1 phi2) : return NNF( phi1 phi2)
phi is (phi1 phi2) : return NNF( phi1 phi2)
phi is phi1 phi2 : return NNF(phi1) NNF(phi2)
phi is phi1 phi2 : return NNF(phi1) NNF(phi2)
end case
end function
Observe that the case clauses only do genuine computation if the root
node of phi is a negation; otherwise, the algorithm simply descents
down phi's parse tree.