src/Tools/Metis/src/Normalize.sig

 (* ========================================================================= *)
 (* NORMALIZING FORMULAS                                                      *)
-(* Copyright (c) 2001-2007 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2001-2009 Joe Hurd, distributed under the BSD License       *)
 (* ========================================================================= *)
 
 signature Normalize =
 sig
 

 (* ------------------------------------------------------------------------- *)
 
 val nnf : Formula.formula -> Formula.formula
 
 (* ------------------------------------------------------------------------- *)
+(* Conjunctive normal form derivations.                                      *)
+(* ------------------------------------------------------------------------- *)
+
+type thm
+
+datatype inference =
+    Axiom of Formula.formula
+  | Definition of string * Formula.formula
+  | Simplify of thm * thm list
+  | Conjunct of thm
+  | Specialize of thm
+  | Skolemize of thm
+  | Clausify of thm
+
+val mkAxiom : Formula.formula -> thm
+
+val destThm : thm -> Formula.formula * inference
+
+val proveThms :
+    thm list -> (Formula.formula * inference * Formula.formula list) list
+
+val toStringInference : inference -> string
+
+val ppInference : inference Print.pp
+
+(* ------------------------------------------------------------------------- *)
 (* Conjunctive normal form.                                                  *)
 (* ------------------------------------------------------------------------- *)
 
-val cnf : Formula.formula -> Formula.formula list
+type cnf
+
+val initialCnf : cnf
+
+val addCnf : thm -> cnf -> (Thm.clause * thm) list * cnf
+
+val proveCnf : thm list -> (Thm.clause * thm) list
+
+val cnf : Formula.formula -> Thm.clause list
 
 end