(* ========================================================================= *)
(* PROOFS IN FIRST ORDER LOGIC *)
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
(* ========================================================================= *)
signature Proof =
sig
(* ------------------------------------------------------------------------- *)
(* A type of first order logic proofs. *)
(* ------------------------------------------------------------------------- *)
datatype inference =
Axiom of LiteralSet.set
| Assume of Atom.atom
| Subst of Subst.subst * Thm.thm
| Resolve of Atom.atom * Thm.thm * Thm.thm
| Refl of Term.term
| Equality of Literal.literal * Term.path * Term.term
type proof = (Thm.thm * inference) list
(* ------------------------------------------------------------------------- *)
(* Reconstructing single inferences. *)
(* ------------------------------------------------------------------------- *)
val inferenceType : inference -> Thm.inferenceType
val parents : inference -> Thm.thm list
val inferenceToThm : inference -> Thm.thm
val thmToInference : Thm.thm -> inference
(* ------------------------------------------------------------------------- *)
(* Reconstructing whole proofs. *)
(* ------------------------------------------------------------------------- *)
val proof : Thm.thm -> proof
(* ------------------------------------------------------------------------- *)
(* Free variables. *)
(* ------------------------------------------------------------------------- *)
val freeIn : Term.var -> proof -> bool
val freeVars : proof -> NameSet.set
(* ------------------------------------------------------------------------- *)
(* Printing. *)
(* ------------------------------------------------------------------------- *)
val ppInference : inference Print.pp
val inferenceToString : inference -> string
val pp : proof Print.pp
val toString : proof -> string
end