1(* ========================================================================= *)
2(* PROOFS IN FIRST ORDER LOGIC                                               *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Proof =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* A type of first order logic proofs.                                       *)
11(* ------------------------------------------------------------------------- *)
12
13datatype inference =
14    Axiom of LiteralSet.set
15  | Assume of Atom.atom
16  | Subst of Subst.subst * Thm.thm
17  | Resolve of Atom.atom * Thm.thm * Thm.thm
18  | Refl of Term.term
19  | Equality of Literal.literal * Term.path * Term.term
20
21type proof = (Thm.thm * inference) list
22
23(* ------------------------------------------------------------------------- *)
24(* Reconstructing single inferences.                                         *)
25(* ------------------------------------------------------------------------- *)
26
27val inferenceType : inference -> Thm.inferenceType
28
29val parents : inference -> Thm.thm list
30
31val inferenceToThm : inference -> Thm.thm
32
33val thmToInference : Thm.thm -> inference
34
35(* ------------------------------------------------------------------------- *)
36(* Reconstructing whole proofs.                                              *)
37(* ------------------------------------------------------------------------- *)
38
39val proof : Thm.thm -> proof
40
41(* ------------------------------------------------------------------------- *)
42(* Free variables.                                                           *)
43(* ------------------------------------------------------------------------- *)
44
45val freeIn : Term.var -> proof -> bool
46
47val freeVars : proof -> NameSet.set
48
49(* ------------------------------------------------------------------------- *)
50(* Printing.                                                                 *)
51(* ------------------------------------------------------------------------- *)
52
53val ppInference : inference Print.pp
54
55val inferenceToString : inference -> string
56
57val pp : proof Print.pp
58
59val toString : proof -> string
60
61end
62