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