1(* ========================================================================= *) 2(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *) 3(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6signature Subsume = 7sig 8 9(* ------------------------------------------------------------------------- *) 10(* A type of clause sets that supports efficient subsumption checking. *) 11(* ------------------------------------------------------------------------- *) 12 13type 'a subsume 14 15val new : unit -> 'a subsume 16 17val size : 'a subsume -> int 18 19val insert : 'a subsume -> Thm.clause * 'a -> 'a subsume 20 21val filter : ('a -> bool) -> 'a subsume -> 'a subsume 22 23val pp : 'a subsume Print.pp 24 25val toString : 'a subsume -> string 26 27(* ------------------------------------------------------------------------- *) 28(* Subsumption checking. *) 29(* ------------------------------------------------------------------------- *) 30 31val subsumes : 32 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 33 (Thm.clause * Subst.subst * 'a) option 34 35val isSubsumed : 'a subsume -> Thm.clause -> bool 36 37val strictlySubsumes : (* exclude subsuming clauses with more literals *) 38 (Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> 39 (Thm.clause * Subst.subst * 'a) option 40 41val isStrictlySubsumed : 'a subsume -> Thm.clause -> bool 42 43(* ------------------------------------------------------------------------- *) 44(* Single clause versions. *) 45(* ------------------------------------------------------------------------- *) 46 47val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option 48 49val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option 50 51end 52