|
0
|
1 |
Provers
|
|
|
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
|
|
|
5 |
certain form are derivable. Unfortunately, little documentation is
|
|
|
6 |
available.
|
|
|
7 |
|
|
|
8 |
classical.ML -- theorem prover for classical logics
|
|
|
9 |
genelim.ML -- bits and pieces for deriving elimination rules
|
|
|
10 |
ind.ML -- a simple induction package
|
|
|
11 |
simp.ML -- a powerful simplifier
|
|
|
12 |
typedsimp.ML -- a rather basic simplifier for explicitly typed logics
|