1(* ========================================================================= *)
2(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS                         *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Thm =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* An abstract type of first order logic theorems.                           *)
11(* ------------------------------------------------------------------------- *)
12
13type thm
14
15(* ------------------------------------------------------------------------- *)
16(* Theorem destructors.                                                      *)
17(* ------------------------------------------------------------------------- *)
18
19type clause = LiteralSet.set
20
21datatype inferenceType =
22    Axiom
23  | Assume
24  | Subst
25  | Factor
26  | Resolve
27  | Refl
28  | Equality
29
30type inference = inferenceType * thm list
31
32val clause : thm -> clause
33
34val inference : thm -> inference
35
36(* Tautologies *)
37
38val isTautology : thm -> bool
39
40(* Contradictions *)
41
42val isContradiction : thm -> bool
43
44(* Unit theorems *)
45
46val destUnit : thm -> Literal.literal
47
48val isUnit : thm -> bool
49
50(* Unit equality theorems *)
51
52val destUnitEq : thm -> Term.term * Term.term
53
54val isUnitEq : thm -> bool
55
56(* Literals *)
57
58val member : Literal.literal -> thm -> bool
59
60val negateMember : Literal.literal -> thm -> bool
61
62(* ------------------------------------------------------------------------- *)
63(* A total order.                                                            *)
64(* ------------------------------------------------------------------------- *)
65
66val compare : thm * thm -> order
67
68val equal : thm -> thm -> bool
69
70(* ------------------------------------------------------------------------- *)
71(* Free variables.                                                           *)
72(* ------------------------------------------------------------------------- *)
73
74val freeIn : Term.var -> thm -> bool
75
76val freeVars : thm -> NameSet.set
77
78(* ------------------------------------------------------------------------- *)
79(* Pretty-printing.                                                          *)
80(* ------------------------------------------------------------------------- *)
81
82val ppInferenceType : inferenceType Print.pp
83
84val inferenceTypeToString : inferenceType -> string
85
86val pp : thm Print.pp
87
88val toString : thm -> string
89
90(* ------------------------------------------------------------------------- *)
91(* Primitive rules of inference.                                             *)
92(* ------------------------------------------------------------------------- *)
93
94(* ------------------------------------------------------------------------- *)
95(*                                                                           *)
96(* ----- axiom C                                                             *)
97(*   C                                                                       *)
98(* ------------------------------------------------------------------------- *)
99
100val axiom : clause -> thm
101
102(* ------------------------------------------------------------------------- *)
103(*                                                                           *)
104(* ----------- assume L                                                      *)
105(*   L \/ ~L                                                                 *)
106(* ------------------------------------------------------------------------- *)
107
108val assume : Literal.literal -> thm
109
110(* ------------------------------------------------------------------------- *)
111(*    C                                                                      *)
112(* -------- subst s                                                          *)
113(*   C[s]                                                                    *)
114(* ------------------------------------------------------------------------- *)
115
116val subst : Subst.subst -> thm -> thm
117
118(* ------------------------------------------------------------------------- *)
119(*   L \/ C    ~L \/ D                                                       *)
120(* --------------------- resolve L                                           *)
121(*        C \/ D                                                             *)
122(*                                                                           *)
123(* The literal L must occur in the first theorem, and the literal ~L must    *)
124(* occur in the second theorem.                                              *)
125(* ------------------------------------------------------------------------- *)
126
127val resolve : Literal.literal -> thm -> thm -> thm
128
129(* ------------------------------------------------------------------------- *)
130(*                                                                           *)
131(* --------- refl t                                                          *)
132(*   t = t                                                                   *)
133(* ------------------------------------------------------------------------- *)
134
135val refl : Term.term -> thm
136
137(* ------------------------------------------------------------------------- *)
138(*                                                                           *)
139(* ------------------------ equality L p t                                   *)
140(*   ~(s = t) \/ ~L \/ L'                                                    *)
141(*                                                                           *)
142(* where s is the subterm of L at path p, and L' is L with the subterm at    *)
143(* path p being replaced by t.                                               *)
144(* ------------------------------------------------------------------------- *)
145
146val equality : Literal.literal -> Term.path -> Term.term -> thm
147
148end
149