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