Convert propositions to NNF, CNF, DNF

normal.sml

type atom = char

type interpretation = atom -> bool

datatype literal = Yes of atom | No of atom

datatype proposition = Literal of literal
                     | Not     of proposition
                     | And     of proposition * proposition
                     | Or      of proposition * proposition
                     | If      of proposition * proposition
                     | Iff     of proposition * proposition

(* eliminate Implications and Bi-implications *)
fun elim (Iff(p,q)) = And(elim(If(p,q)),elim(If(q,p)))
  | elim (If (p,q)) = Or(Not(elim(p)),elim(q))
  | elim p          = p

(* push negations in until the apply only to atoms. pushN assumes that the
 * proposition has already been elim'd, i.e. contains only Literals, Not, And,
 * Or.*)
fun pushN (Not(Not(p)))          = pushN(p)
  | pushN (Not(Literal(No(a))))  = Literal(Yes(a))                 (* base 1 *)
  | pushN (Not(Literal(Yes(a)))) = Literal(No(a))                  (* base 2 *)
  | pushN (Not(And(p,q)))        = Or(pushN(Not(p)),pushN(Not(q)))
  | pushN (Not(Or(p,q)))         = And(pushN(Not(p)),pushN(Not(q)))
  | pushN (And(p,q))             = And(pushN(p),pushN(q))
  | pushN (Or(p,q))              = Or(pushN(p),pushN(q))
  | pushN (Literal(l))           = Literal(l)                      (* base 3 *)

(* push disjunctions in. pushD assumes that the proposition has already been
 * pushN'd, i.e. contains only Literals, And, Or. *)
fun pushD (Or(p,And(q,r))) = And(pushD(Or(p,q)),pushD(Or(p,r)))
  | pushD (Or(And(q,r),p)) = And(pushD(Or(p,q)),pushD(Or(p,r)))
  | pushD (Or(p,q))        = Or(pushD(p),pushD(q))
  | pushD (Literal(l))     = Literal(l)
  | pushD (And(p,q))       = And(pushD(p),pushD(q))

(* push conjunctions in. pushC assumes that the proposition has already been
 * pushN'd, i.e. contains only Literals, And, Or. *)
fun pushC (And(p,Or(q,r))) = Or(pushC(And(p,q)),pushC(And(p,r)))
  | pushC (And(Or(q,r),p)) = Or(pushC(And(p,q)),pushC(And(p,r)))
  | pushC (And(p,q))       = And(pushC(p),pushC(q))
  | pushC (Literal(l))     = Literal(l)
  | pushC (Or(p,q))        = Or(pushC(p),pushC(q))

(* test whether a proposition p is valid under an interpretation i *)
fun test p (i:interpretation) =
  let fun test_helper (Literal(Yes a)) = i a
        | test_helper (Literal(No a))  = not (i a)
        | test_helper (Not(q))         = not (test_helper q)
        | test_helper (And(q,r))       = test_helper(q) andalso test_helper(r)
        | test_helper (Or(q,r))        = test_helper(q) orelse test_helper(r)
  in test_helper (elim p) end

fun nnf p = pushN(elim p)   (* Negation Normal Form *)
fun cnf p = pushD(nnf p)    (* Conjunctive Normal Form *)
fun dnf p = pushC(nnf p)    (* Disjunctive Normal Form *)

val p = Literal (Yes #"P")
val q = Literal (Yes #"Q")
val r = Literal (Yes #"R")

val p1 = If(Or(p,q),Or(q,p))
val p2 = If(And(p,q),And(q,p))
val p3 = If(If(If(p,q),p),p)

Try running the cnf for the following. You won't get correct results:
let prop8 = Or(Or(And(Var 'a', Var 'b'), And(Var 'c', Var 'd')), And(Var 'e', Var 'f'));;

You need to handle Or(a, b) case more appropriately.