|
4289
|
1 |
|
|
|
2 |
Provers
|
|
0
|
3 |
|
|
|
4 |
This directory contains ML sources of generic theorem proving tools.
|
|
|
5 |
Typically, they can be applied to various logics, provided rules of a
|
|
3279
|
6 |
certain form are derivable. Some of these are documented in the
|
|
195
|
7 |
Reference Manual.
|
|
0
|
8 |
|
|
4289
|
9 |
blast.ML -- generic tableau prover with proof reconstruction
|
|
|
10 |
classical.ML -- theorem prover for classical logics
|
|
|
11 |
genelim.ML -- bits and pieces for deriving elimination rules
|
|
|
12 |
hypsubst.ML -- tactic to substitute in the hypotheses
|
|
|
13 |
ind.ML -- a simple induction package
|
|
|
14 |
simp.ML -- powerful but slow simplifier
|
|
|
15 |
simplifier.ML -- fast simplifier
|
|
|
16 |
splitter.ML -- performs case splits for simplifier.ML
|
|
|
17 |
typedsimp.ML -- basic simplifier for explicitly typed logics
|
|
|
18 |
|
|
|
19 |
directory Arith:
|
|
|
20 |
nat_transitive.ML -- simple package for inequalities over nat
|
|
|
21 |
|
|
|
22 |
|
|
|
23 |
$Id$
|