(* ========================================================================= *) (* A LOGICAL KERNEL FOR FIRST ORDER CLAUSAL THEOREMS *) (* Copyright (c) 2001 Joe Leslie-Hurd, distributed under the MIT license *) (* ========================================================================= *) signature Thm = sig (* ------------------------------------------------------------------------- *) (* An abstract type of first order logic theorems. *) (* ------------------------------------------------------------------------- *) type thm (* ------------------------------------------------------------------------- *) (* Primitive rules of inference. *) (* ------------------------------------------------------------------------- *) (* ------------------------------------------------------------------------- *) (* *) (* ----- axiom C *) (* C *) (* ------------------------------------------------------------------------- *) val axiom : clause -> thm (* ------------------------------------------------------------------------- *) (* *) (* ----------- assume L *) (* L \/ ~L *) (* ------------------------------------------------------------------------- *) val assume : literal -> thm (* ------------------------------------------------------------------------- *) (* C *) (* -------- subst s *) (* C[s] *) (* ------------------------------------------------------------------------- *) val subst : subst -> thm -> thm (* ------------------------------------------------------------------------- *) (* L \/ C ~L \/ D *) (* --------------------- resolve L *) (* C \/ D *) (* *) (* The literal L must occur in the first theorem, and the literal ~L must *) (* occur in the second theorem. *) (* ------------------------------------------------------------------------- *) val resolve : literal -> thm -> thm -> thm (* ------------------------------------------------------------------------- *) (* *) (* --------- refl t *) (* t = t *) (* ------------------------------------------------------------------------- *) val refl : term -> thm (* ------------------------------------------------------------------------- *) (* *) (* ------------------------ equality L p t *) (* ~(s = t) \/ ~L \/ L' *) (* *) (* where s is the subterm of L at path p, and L' is L with the subterm at *) (* path p being replaced by t. *) (* ------------------------------------------------------------------------- *) val equality : literal -> path -> term -> thm end