1(* ========================================================================= *) 2(* THE RESOLUTION PROOF PROCEDURE *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Resolution :> Resolution = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* A type of resolution proof procedures. *) 13(* ------------------------------------------------------------------------- *) 14 15type parameters = 16 {active : Active.parameters, 17 waiting : Waiting.parameters}; 18 19datatype resolution = 20 Resolution of 21 {parameters : parameters, 22 active : Active.active, 23 waiting : Waiting.waiting}; 24 25(* ------------------------------------------------------------------------- *) 26(* Basic operations. *) 27(* ------------------------------------------------------------------------- *) 28 29val default : parameters = 30 {active = Active.default, 31 waiting = Waiting.default}; 32 33fun new parameters ths = 34 let 35 val {active = activeParm, waiting = waitingParm} = parameters 36 37 val (active,cls) = Active.new activeParm ths (* cls = factored ths *) 38 39 val waiting = Waiting.new waitingParm cls 40 in 41 Resolution {parameters = parameters, active = active, waiting = waiting} 42 end 43(*MetisDebug 44 handle e => 45 let 46 val () = Print.trace Print.ppException "Resolution.new: exception" e 47 in 48 raise e 49 end; 50*) 51 52fun active (Resolution {active = a, ...}) = a; 53 54fun waiting (Resolution {waiting = w, ...}) = w; 55 56val pp = 57 Print.ppMap 58 (fn Resolution {active,waiting,...} => 59 "Resolution(" ^ Int.toString (Active.size active) ^ 60 "<-" ^ Int.toString (Waiting.size waiting) ^ ")") 61 Print.ppString; 62 63(* ------------------------------------------------------------------------- *) 64(* The main proof loop. *) 65(* ------------------------------------------------------------------------- *) 66 67datatype decision = 68 Contradiction of Thm.thm 69 | Satisfiable of Thm.thm list; 70 71datatype state = 72 Decided of decision 73 | Undecided of resolution; 74 75fun iterate res = 76 let 77 val Resolution {parameters,active,waiting} = res 78 79(*MetisTrace2 80 val () = Print.trace Active.pp "Resolution.iterate: active" active 81 val () = Print.trace Waiting.pp "Resolution.iterate: waiting" waiting 82*) 83 in 84 case Waiting.remove waiting of 85 NONE => 86 let 87 val sat = Satisfiable (List.map Clause.thm (Active.saturation active)) 88 in 89 Decided sat 90 end 91 | SOME ((d,cl),waiting) => 92 if Clause.isContradiction cl then 93 Decided (Contradiction (Clause.thm cl)) 94 else 95 let 96(*MetisTrace1 97 val () = Print.trace Clause.pp "Resolution.iterate: cl" cl 98*) 99 val (active,cls) = Active.add active cl 100 101 val waiting = Waiting.add waiting (d,cls) 102 103 val res = 104 Resolution 105 {parameters = parameters, 106 active = active, 107 waiting = waiting} 108 in 109 Undecided res 110 end 111 end; 112 113fun loop res = 114 case iterate res of 115 Decided dec => dec 116 | Undecided res => loop res; 117 118end 119