| author | blanchet |
| Thu, 22 Oct 2009 16:34:49 +0200 | |
| changeset 33194 | 13450310a776 |
| parent 23510 | 4521fead5609 |
| child 39353 | 7f11d833d65b |
| permissions | -rw-r--r-- |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
1 |
(* ========================================================================= *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
2 |
(* SUBSUMPTION CHECKING FOR FIRST ORDER LOGIC CLAUSES *) |
| 23510 | 3 |
(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
4 |
(* ========================================================================= *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
5 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
6 |
signature Subsume = |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
7 |
sig |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
8 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
9 |
(* ------------------------------------------------------------------------- *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
10 |
(* A type of clause sets that supports efficient subsumption checking. *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
(* ------------------------------------------------------------------------- *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
12 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
13 |
type 'a subsume |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
14 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
15 |
val new : unit -> 'a subsume |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
16 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
17 |
val size : 'a subsume -> int |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
18 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
19 |
val insert : 'a subsume -> Thm.clause * 'a -> 'a subsume |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
20 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
val filter : ('a -> bool) -> 'a subsume -> 'a subsume
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
22 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
23 |
val pp : 'a subsume Parser.pp |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
24 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
25 |
val toString : 'a subsume -> string |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
26 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
27 |
(* ------------------------------------------------------------------------- *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
28 |
(* Subsumption checking. *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
29 |
(* ------------------------------------------------------------------------- *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
30 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
31 |
val subsumes : |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
32 |
(Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
33 |
(Thm.clause * Subst.subst * 'a) option |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
34 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
35 |
val isSubsumed : 'a subsume -> Thm.clause -> bool |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
36 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
37 |
val strictlySubsumes : (* exclude subsuming clauses with more literals *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
38 |
(Thm.clause * Subst.subst * 'a -> bool) -> 'a subsume -> Thm.clause -> |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
39 |
(Thm.clause * Subst.subst * 'a) option |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
40 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
41 |
val isStrictlySubsumed : 'a subsume -> Thm.clause -> bool |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
42 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
43 |
(* ------------------------------------------------------------------------- *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
44 |
(* Single clause versions. *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
45 |
(* ------------------------------------------------------------------------- *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
46 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
47 |
val clauseSubsumes : Thm.clause -> Thm.clause -> Subst.subst option |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
48 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
49 |
val clauseStrictlySubsumes : Thm.clause -> Thm.clause -> Subst.subst option |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
50 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
51 |
end |