Convert Sentences to Implicative Normal Form

Once is in conjunctive normal form, it is easy to convert it in implicative normal form. The function does exactly that. It first calls and then collects positive literals and negative literals into two list and puts the negative literals on the left hand side, positive literals on the right hand side of the connectiv, where the literals on the LHS are connected conjunctions and the literals on the RHS are connected by disjunctions.

$$\begin{eqnarray*} \neg a\vee \neg b\vee c\vee d & becomes & a\wedge b\Rightarrow c\vee d \end{eqnarray*}$$