1(* ========================================================================= *) 2(* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Thm = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* An abstract type of first order logic theorems. *) 11(* ------------------------------------------------------------------------- *) 12 13type thm 14 15(* ------------------------------------------------------------------------- *) 16(* Theorem destructors. *) 17(* ------------------------------------------------------------------------- *) 18 19type clause = LiteralSet.set 20 21datatype inferenceType = 22 Axiom 23 | Assume 24 | Subst 25 | Factor 26 | Resolve 27 | Refl 28 | Equality 29 30type inference = inferenceType * thm list 31 32val clause : thm -> clause 33 34val inference : thm -> inference 35 36(* Tautologies *) 37 38val isTautology : thm -> bool 39 40(* Contradictions *) 41 42val isContradiction : thm -> bool 43 44(* Unit theorems *) 45 46val destUnit : thm -> Literal.literal 47 48val isUnit : thm -> bool 49 50(* Unit equality theorems *) 51 52val destUnitEq : thm -> Term.term * Term.term 53 54val isUnitEq : thm -> bool 55 56(* Literals *) 57 58val member : Literal.literal -> thm -> bool 59 60val negateMember : Literal.literal -> thm -> bool 61 62(* ------------------------------------------------------------------------- *) 63(* A total order. *) 64(* ------------------------------------------------------------------------- *) 65 66val compare : thm * thm -> order 67 68val equal : thm -> thm -> bool 69 70(* ------------------------------------------------------------------------- *) 71(* Free variables. *) 72(* ------------------------------------------------------------------------- *) 73 74val freeIn : Term.var -> thm -> bool 75 76val freeVars : thm -> NameSet.set 77 78(* ------------------------------------------------------------------------- *) 79(* Pretty-printing. *) 80(* ------------------------------------------------------------------------- *) 81 82val ppInferenceType : inferenceType Print.pp 83 84val inferenceTypeToString : inferenceType -> string 85 86val pp : thm Print.pp 87 88val toString : thm -> string 89 90(* ------------------------------------------------------------------------- *) 91(* Primitive rules of inference. *) 92(* ------------------------------------------------------------------------- *) 93 94(* ------------------------------------------------------------------------- *) 95(* *) 96(* ----- axiom C *) 97(* C *) 98(* ------------------------------------------------------------------------- *) 99 100val axiom : clause -> thm 101 102(* ------------------------------------------------------------------------- *) 103(* *) 104(* ----------- assume L *) 105(* L \/ ~L *) 106(* ------------------------------------------------------------------------- *) 107 108val assume : Literal.literal -> thm 109 110(* ------------------------------------------------------------------------- *) 111(* C *) 112(* -------- subst s *) 113(* C[s] *) 114(* ------------------------------------------------------------------------- *) 115 116val subst : Subst.subst -> thm -> thm 117 118(* ------------------------------------------------------------------------- *) 119(* L \/ C ~L \/ D *) 120(* --------------------- resolve L *) 121(* C \/ D *) 122(* *) 123(* The literal L must occur in the first theorem, and the literal ~L must *) 124(* occur in the second theorem. *) 125(* ------------------------------------------------------------------------- *) 126 127val resolve : Literal.literal -> thm -> thm -> thm 128 129(* ------------------------------------------------------------------------- *) 130(* *) 131(* --------- refl t *) 132(* t = t *) 133(* ------------------------------------------------------------------------- *) 134 135val refl : Term.term -> thm 136 137(* ------------------------------------------------------------------------- *) 138(* *) 139(* ------------------------ equality L p t *) 140(* ~(s = t) \/ ~L \/ L' *) 141(* *) 142(* where s is the subterm of L at path p, and L' is L with the subterm at *) 143(* path p being replaced by t. *) 144(* ------------------------------------------------------------------------- *) 145 146val equality : Literal.literal -> Term.path -> Term.term -> thm 147 148end 149