author | wenzelm |
Mon, 17 Apr 2000 14:27:10 +0200 | |
changeset 8731 | 085f0e32b9d6 |
parent 5897 | b3548f939dd2 |
child 8870 | e900a58cafe4 |
permissions | -rw-r--r-- |
4623 | 1 |
Provers: generic theorem proving tools |
0 | 2 |
|
3 |
This directory contains ML sources of generic theorem proving tools. |
|
4 |
Typically, they can be applied to various logics, provided rules of a |
|
3279 | 5 |
certain form are derivable. Some of these are documented in the |
195 | 6 |
Reference Manual. |
0 | 7 |
|
4623 | 8 |
blast.ML generic tableau prover with proof reconstruction |
4654 | 9 |
clasimp.ML combination of classical reasoner and simplifier |
4623 | 10 |
classical.ML theorem prover for classical logics |
11 |
hypsubst.ML tactic to substitute in the hypotheses |
|
12 |
ind.ML a simple induction package |
|
13 |
quantifier1.ML simplification procedures for "1 point rules" |
|
14 |
simp.ML powerful but slow simplifier |
|
15 |
simplifier.ML fast simplifier |
|
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
4654
diff
changeset
|
16 |
split_paired_all.ML turn surjective pairing into split rule |
4623 | 17 |
splitter.ML performs case splits for simplifier.ML |
18 |
typedsimp.ML basic simplifier for explicitly typed logics |
|
4289 | 19 |
|
20 |
directory Arith: |
|
4623 | 21 |
cancel_factor.ML cancel common constant factor |
22 |
cancel_sums.ML cancel common summands |
|
23 |
nat_transitive.ML simple package for inequalities over nat |