equal
deleted
inserted
replaced
1 (* ========================================================================= *) |
1 (* ========================================================================= *) |
2 (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSES *) |
2 (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *) |
3 (* Copyright (c) 2001-2004 Joe Hurd, distributed under the BSD License *) |
3 (* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) |
4 (* ========================================================================= *) |
4 (* ========================================================================= *) |
5 |
5 |
6 signature Thm = |
6 signature Thm = |
7 sig |
7 sig |
8 |
8 |
9 (* ------------------------------------------------------------------------- *) |
9 (* ------------------------------------------------------------------------- *) |
10 (* An abstract type of first order logic theorems. *) |
10 (* An abstract type of first order logic theorems. *) |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 |
|
13 type thm |
|
14 |
|
15 (* ------------------------------------------------------------------------- *) |
|
16 (* Theorem destructors. *) |
11 (* ------------------------------------------------------------------------- *) |
17 (* ------------------------------------------------------------------------- *) |
12 |
18 |
13 type clause = LiteralSet.set |
19 type clause = LiteralSet.set |
14 |
20 |
15 datatype inferenceType = |
21 datatype inferenceType = |
19 | Factor |
25 | Factor |
20 | Resolve |
26 | Resolve |
21 | Refl |
27 | Refl |
22 | Equality |
28 | Equality |
23 |
29 |
24 type thm |
|
25 |
|
26 type inference = inferenceType * thm list |
30 type inference = inferenceType * thm list |
27 |
|
28 (* ------------------------------------------------------------------------- *) |
|
29 (* Theorem destructors. *) |
|
30 (* ------------------------------------------------------------------------- *) |
|
31 |
31 |
32 val clause : thm -> clause |
32 val clause : thm -> clause |
33 |
33 |
34 val inference : thm -> inference |
34 val inference : thm -> inference |
35 |
35 |
77 |
77 |
78 (* ------------------------------------------------------------------------- *) |
78 (* ------------------------------------------------------------------------- *) |
79 (* Pretty-printing. *) |
79 (* Pretty-printing. *) |
80 (* ------------------------------------------------------------------------- *) |
80 (* ------------------------------------------------------------------------- *) |
81 |
81 |
82 val ppInferenceType : inferenceType Parser.pp |
82 val ppInferenceType : inferenceType Print.pp |
83 |
83 |
84 val inferenceTypeToString : inferenceType -> string |
84 val inferenceTypeToString : inferenceType -> string |
85 |
85 |
86 val pp : thm Parser.pp |
86 val pp : thm Print.pp |
87 |
87 |
88 val toString : thm -> string |
88 val toString : thm -> string |
89 |
89 |
90 (* ------------------------------------------------------------------------- *) |
90 (* ------------------------------------------------------------------------- *) |
91 (* Primitive rules of inference. *) |
91 (* Primitive rules of inference. *) |