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

3279

5 
certain form are derivable. Some of these are documented in the

195

6 
Reference Manual.

0

7 

4623

8 
blast.ML generic tableau prover with proof reconstruction

4654

9 
clasimp.ML combination of classical reasoner and simplifier

4623

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 
quantifier1.ML simplification procedures for "1 point rules"


15 
simp.ML powerful but slow simplifier


16 
simplifier.ML fast simplifier


17 
splitter.ML performs case splits for simplifier.ML


18 
typedsimp.ML basic simplifier for explicitly typed logics

4289

19 


20 
directory Arith:

4623

21 
cancel_factor.ML cancel common constant factor


22 
cancel_sums.ML cancel common summands


23 
nat_transitive.ML simple package for inequalities over nat
