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.

• distributivity law;
• conjunctive normal form.