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