1(* ========================================================================= *) 2(* THE RESOLUTION PROOF PROCEDURE *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Resolution = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* A type of resolution proof procedures. *) 11(* ------------------------------------------------------------------------- *) 12 13type parameters = 14 {active : Active.parameters, 15 waiting : Waiting.parameters} 16 17type resolution 18 19(* ------------------------------------------------------------------------- *) 20(* Basic operations. *) 21(* ------------------------------------------------------------------------- *) 22 23val default : parameters 24 25val new : 26 parameters -> {axioms : Thm.thm list, conjecture : Thm.thm list} -> 27 resolution 28 29val active : resolution -> Active.active 30 31val waiting : resolution -> Waiting.waiting 32 33val pp : resolution Print.pp 34 35(* ------------------------------------------------------------------------- *) 36(* The main proof loop. *) 37(* ------------------------------------------------------------------------- *) 38 39datatype decision = 40 Contradiction of Thm.thm 41 | Satisfiable of Thm.thm list 42 43datatype state = 44 Decided of decision 45 | Undecided of resolution 46 47val iterate : resolution -> state 48 49val loop : resolution -> decision 50 51end 52