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