|
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
|
|
30159
|
5 |
certain form are derivable.
|
|
0
|
6 |
|
|
4623
|
7 |
blast.ML generic tableau prover with proof reconstruction
|
|
4654
|
8 |
clasimp.ML combination of classical reasoner and simplifier
|
|
4623
|
9 |
classical.ML theorem prover for classical logics
|
|
|
10 |
hypsubst.ML tactic to substitute in the hypotheses
|
|
|
11 |
quantifier1.ML simplification procedures for "1 point rules"
|
|
16019
|
12 |
splitter.ML performs case splits for simplifier
|
|
4623
|
13 |
typedsimp.ML basic simplifier for explicitly typed logics
|
|
4289
|
14 |
|
|
|
15 |
directory Arith:
|
|
8870
|
16 |
assoc_fold.ML fold numerals in nested products
|
|
|
17 |
cancel_numerals.ML cancel common coefficients in balanced expressions
|
|
4623
|
18 |
cancel_sums.ML cancel common summands
|
|
8870
|
19 |
combine_numerals.ML combine coefficients in expressions
|
|
|
20 |
fast_lin_arith.ML generic linear arithmetic package
|