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


9 
classical.ML theorem prover for classical logics


10 
genelim.ML bits and pieces for deriving elimination rules


11 
hypsubst.ML tactic to substitute in the hypotheses


12 
ind.ML a simple induction package


13 
quantifier1.ML simplification procedures for "1 point rules"


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

4289

18 


19 
directory Arith:

4623

20 
cancel_factor.ML cancel common constant factor


21 
cancel_sums.ML cancel common summands


22 
nat_transitive.ML simple package for inequalities over nat
