152419Sjulian(* ========================================================================= *)
252419Sjulian(* PROOFS IN FIRST ORDER LOGIC                                               *)
352419Sjulian(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
452419Sjulian(* ========================================================================= *)
559882Sarchie
652419Sjuliansignature Proof =
752419Sjuliansig
852419Sjulian
952419Sjulian(* ------------------------------------------------------------------------- *)
1052419Sjulian(* A type of first order logic proofs.                                       *)
1152419Sjulian(* ------------------------------------------------------------------------- *)
1252419Sjulian
1352419Sjuliandatatype inference =
1452419Sjulian    Axiom of LiteralSet.set
1552419Sjulian  | Assume of Atom.atom
1652419Sjulian  | Subst of Subst.subst * Thm.thm
1752419Sjulian  | Resolve of Atom.atom * Thm.thm * Thm.thm
1852419Sjulian  | Refl of Term.term
1952419Sjulian  | Equality of Literal.literal * Term.path * Term.term
2052419Sjulian
2152419Sjuliantype proof = (Thm.thm * inference) list
2252419Sjulian
2352419Sjulian(* ------------------------------------------------------------------------- *)
2452419Sjulian(* Reconstructing single inferences.                                         *)
2552419Sjulian(* ------------------------------------------------------------------------- *)
2652419Sjulian
2752419Sjulianval inferenceType : inference -> Thm.inferenceType
2852419Sjulian
2952419Sjulianval parents : inference -> Thm.thm list
3052419Sjulian
3152419Sjulianval inferenceToThm : inference -> Thm.thm
3252419Sjulian
3352419Sjulianval thmToInference : Thm.thm -> inference
3452419Sjulian
3552419Sjulian(* ------------------------------------------------------------------------- *)
3652419Sjulian(* Reconstructing whole proofs.                                              *)
3752419Sjulian(* ------------------------------------------------------------------------- *)
3852419Sjulian
3952419Sjulianval proof : Thm.thm -> proof
4052419Sjulian
4152419Sjulian(* ------------------------------------------------------------------------- *)
4252419Sjulian(* Free variables.                                                           *)
4352419Sjulian(* ------------------------------------------------------------------------- *)
4452419Sjulian
4552419Sjulianval freeIn : Term.var -> proof -> bool
4652419Sjulian
4752419Sjulianval freeVars : proof -> NameSet.set
4859882Sarchie
4952419Sjulian(* ------------------------------------------------------------------------- *)
5052639Sarchie(* Printing.                                                                 *)
5152639Sarchie(* ------------------------------------------------------------------------- *)
5252639Sarchie
5352639Sarchieval ppInference : inference Print.pp
5452639Sarchie
5552639Sarchieval inferenceToString : inference -> string
5652639Sarchie
5752639Sarchieval pp : proof Print.pp
5852639Sarchie
5952639Sarchieval toString : proof -> string
6052419Sjulian
6152639Sarchieend
6252639Sarchie