CIS 301. Computing an implication-free formula.

function IMPL_FREE(phi)

 precondition: phi is a formula of propositional logic with generating gammar 
 phi ::= p |  phi | phi  phi | phi  phi | phi  phi 

 postcondition: IMPL_FREE(phi) computes an equivalent and implication-free formula 

  begin function
	case
	  phi is a literal : return phi
	  phi is phi1 : return  IMPL_FREE(phi1)
	  phi is phi1  phi2 : return IMPL_FREE(phi1)  IMPL_FREE(phi2)
	  phi is phi1  phi2 : return IMPL_FREE(phi1)  IMPL_FREE(phi2)
	  phi is phi1  phi2 : return IMPL_FREE ( phi1   phi2)
	end case
  end function


 Observe that only the last clauses does genuine computation; all other 
 clauses simply pass on control to the formula's immediate subtree(s). 
 As for the last clause, we use the equivalence between "phi1  phi2" 
 and " pih1  phi2" to obtain an argument for the recursive call. 

• negation normal form;
• distributivity law;
• conjunctive normal form.