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