src/Tools/Metis/src/Resolution.sig

+(* ========================================================================= *)
+(* THE RESOLUTION PROOF PROCEDURE                                            *)
+(* Copyright (c) 2001-2007 Joe Hurd, distributed under the GNU GPL version 2 *)
+(* ========================================================================= *)
+
+signature Resolution =
+sig
+
+(* ------------------------------------------------------------------------- *)
+(* A type of resolution proof procedures.                                    *)
+(* ------------------------------------------------------------------------- *)
+
+type parameters =
+     {active : Active.parameters,
+      waiting : Waiting.parameters}
+
+type resolution
+
+(* ------------------------------------------------------------------------- *)
+(* Basic operations.                                                         *)
+(* ------------------------------------------------------------------------- *)
+
+val default : parameters
+
+val new :
+    parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} ->
+    resolution
+
+val active : resolution -> Active.active
+
+val waiting : resolution -> Waiting.waiting
+
+val pp : resolution Print.pp
+
+(* ------------------------------------------------------------------------- *)
+(* The main proof loop.                                                      *)
+(* ------------------------------------------------------------------------- *)
+
+datatype decision =
+    Contradiction of Thm.thm
+  | Satisfiable of Thm.thm list
+
+datatype state =
+    Decided of decision
+  | Undecided of resolution
+
+val iterate : resolution -> state
+
+val loop : resolution -> decision
+
+end