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 
abel_cancel.ML cancel complementary terms in sums of Abelian groups


17 
assoc_fold.ML fold numerals in nested products


18 
cancel_numerals.ML cancel common coefficients in balanced expressions

4623

19 
cancel_factor.ML cancel common constant factor


20 
cancel_sums.ML cancel common summands

8870

21 
combine_numerals.ML combine coefficients in expressions


22 
fast_lin_arith.ML generic linear arithmetic package
