| author | wenzelm |
| Mon, 13 Apr 2020 22:08:14 +0200 | |
| changeset 71751 | abf3e80bd815 |
| parent 39502 | cffceed8e7fa |
| child 72004 | 913162a47d9f |
| 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 |
(* THE KNUTH-BENDIX TERM ORDERING *) |
| 39502 | 3 |
(* Copyright (c) 2002 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 KnuthBendixOrder = |
|
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 |
(* The weight of all constants must be at least 1, and there must be at most *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
(* one unary function with weight 0. *) |
|
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 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
14 |
type kbo = |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
15 |
{weight : Term.function -> int,
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
16 |
precedence : Term.function * Term.function -> order} |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
17 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
18 |
val default : kbo |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
19 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
20 |
val compare : kbo -> Term.term * Term.term -> order option |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
22 |
end |