(* ========================================================================= *)
(* NORMALIZING FORMULAS *)
(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Normalize =
sig
(* ------------------------------------------------------------------------- *)
(* Negation normal form. *)
(* ------------------------------------------------------------------------- *)
val nnf : Formula.formula -> Formula.formula
(* ------------------------------------------------------------------------- *)
(* Conjunctive normal form. *)
(* ------------------------------------------------------------------------- *)
val cnf : Formula.formula -> Formula.formula list
end