CIS 301. Computing a conjunctive normal form.

function CNF(phi):

 precondition: phi implication free and in nnf  with generating gammar 
 phi ::= L | phi  phi | phi  phi 
 postcondition: CNF(phi) computes an equivalent cnf for phi 

  begin function
      case
	phi is a literal L  : return L
	phi is phi1  phi2 : return CNF(phi1)  CNF(phi)
	phi is phi1  phi2 : return DIST(CNF(phi1),CNF(phi2))
	end case
  end function}

 The precondition of the algorithm ensures that phi could only have   
 three possible root nodes: if the root is a negation, we have the    
 first case; if it is a conjunction, the second; if disjunction, the  
 third one.								

 We may compute the cnf of a conjunction by first computing cnfs for  
 each conjunct and then forming their conjunction.		        
 The computation of a cnf for a disjunction also computes cnfs for    
 its two arguments, but we have to rely on a function DIST that       
 "animates" the distributivity law; if we simply returned		
 CNF(phi1)  CNF(phi2), then this would not be a cnf if one of its    
 arguments were a conjunction, which is generally the case.		

• distributivity law;
• negation normal form.