author | wenzelm |
Thu, 02 Oct 2008 19:59:00 +0200 | |
changeset 28464 | dcc030b52583 |
parent 16019 | 0e1405402d53 |
child 30159 | 7b55b6b5c0c2 |
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 |
|
11840
54fe56353704
induct_method.ML -- proof by cases and induction on sets and types (Isar);
wenzelm
parents:
8870
diff
changeset
|
13 |
induct_method.ML proof by cases and induction on sets and types (Isar) |
13736
6ea0e7c43c4f
Transitivity reasoner renamed to linorder.ML. README updated.
ballarin
parents:
13735
diff
changeset
|
14 |
linorder.ML transitivity reasoner for linear (total) orders |
4623 | 15 |
quantifier1.ML simplification procedures for "1 point rules" |
16 |
simp.ML powerful but slow simplifier |
|
5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
4654
diff
changeset
|
17 |
split_paired_all.ML turn surjective pairing into split rule |
16019 | 18 |
splitter.ML performs case splits for simplifier |
4623 | 19 |
typedsimp.ML basic simplifier for explicitly typed logics |
4289 | 20 |
|
21 |
directory Arith: |
|
8870 | 22 |
abel_cancel.ML cancel complementary terms in sums of Abelian groups |
23 |
assoc_fold.ML fold numerals in nested products |
|
24 |
cancel_numerals.ML cancel common coefficients in balanced expressions |
|
4623 | 25 |
cancel_factor.ML cancel common constant factor |
26 |
cancel_sums.ML cancel common summands |
|
8870 | 27 |
combine_numerals.ML combine coefficients in expressions |
28 |
fast_lin_arith.ML generic linear arithmetic package |