1(* ========================================================================= *) 2(* A LCF-STYLE LOGICAL KERNEL FOR FIRST-ORDER CLAUSES *) 3(* Copyright (c) 2001-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6signature mlibKernel = 7sig 8 9type term = mlibTerm.term 10type formula = mlibTerm.formula 11type subst = mlibSubst.subst 12 13(* An ABSTRACT type for theorems *) 14eqtype thm 15datatype inference = Axiom | Refl | Assume | Inst | Factor | Resolve | Equality 16 17(* Destruction of theorems is fine *) 18val dest_thm : thm -> formula list * (inference * thm list) 19 20(* But creation is only allowed by the primitive rules of inference *) 21val AXIOM : formula list -> thm 22val REFL : term -> thm 23val ASSUME : formula -> thm 24val INST : subst -> thm -> thm 25val FACTOR : thm -> thm 26val RESOLVE : formula -> thm -> thm -> thm 27val EQUALITY : formula -> int list -> term -> bool -> thm -> thm 28 29end 30