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