1 Provers: generic theorem proving tools |
1 Provers: generic theorem proving tools |
2 |
2 |
3 This directory contains ML sources of generic theorem proving tools. |
3 This directory contains ML sources of generic theorem proving tools. |
4 Typically, they can be applied to various logics, provided rules of a |
4 Typically, they can be applied to various logics, provided rules of a |
5 certain form are derivable. Some of these are documented in the |
5 certain form are derivable. |
6 Reference Manual. |
|
7 |
6 |
8 blast.ML generic tableau prover with proof reconstruction |
7 blast.ML generic tableau prover with proof reconstruction |
9 clasimp.ML combination of classical reasoner and simplifier |
8 clasimp.ML combination of classical reasoner and simplifier |
10 classical.ML theorem prover for classical logics |
9 classical.ML theorem prover for classical logics |
11 hypsubst.ML tactic to substitute in the hypotheses |
10 hypsubst.ML tactic to substitute in the hypotheses |
12 ind.ML a simple induction package |
|
13 induct_method.ML proof by cases and induction on sets and types (Isar) |
|
14 linorder.ML transitivity reasoner for linear (total) orders |
|
15 quantifier1.ML simplification procedures for "1 point rules" |
11 quantifier1.ML simplification procedures for "1 point rules" |
16 simp.ML powerful but slow simplifier |
|
17 split_paired_all.ML turn surjective pairing into split rule |
|
18 splitter.ML performs case splits for simplifier |
12 splitter.ML performs case splits for simplifier |
19 typedsimp.ML basic simplifier for explicitly typed logics |
13 typedsimp.ML basic simplifier for explicitly typed logics |
20 |
14 |
21 directory Arith: |
15 directory Arith: |
22 abel_cancel.ML cancel complementary terms in sums of Abelian groups |
16 abel_cancel.ML cancel complementary terms in sums of Abelian groups |