equal
deleted
inserted
replaced
1 Provers |
1 Provers |
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. Unfortunately, little documentation is |
5 certain form are derivable. The first three are documented in the |
6 available. |
6 Reference Manual. |
7 |
7 |
8 classical.ML -- theorem prover for classical logics |
8 classical.ML -- theorem prover for classical logics |
9 genelim.ML -- bits and pieces for deriving elimination rules |
9 hypsubst.ML -- tactic to substitute in the hypotheses |
10 ind.ML -- a simple induction package |
10 simplifier.ML -- fast simplifier |
11 simp.ML -- a powerful simplifier |
11 simp.ML -- powerful but slow simplifier |
12 typedsimp.ML -- a rather basic simplifier for explicitly typed logics |
12 typedsimp.ML -- basic simplifier for explicitly typed logics |
|
13 splitter.ML -- performs case splits for simplifier.ML |
|
14 genelim.ML -- bits and pieces for deriving elimination rules |
|
15 ind.ML -- a simple induction package |