author  paulson 
Fri, 12 May 2000 15:21:58 +0200  
changeset 8870  e900a58cafe4 
parent 5897  b3548f939dd2 
child 11840  54fe56353704 
permissions  rwrr 
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 
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 

5680
4f526bcd3a68
split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents:
4654
diff
changeset

16 
split_paired_all.ML turn surjective pairing into split rule 
4623  17 
splitter.ML performs case splits for simplifier.ML 
18 
typedsimp.ML basic simplifier for explicitly typed logics 

4289  19 

20 
directory Arith: 

8870  21 
abel_cancel.ML cancel complementary terms in sums of Abelian groups 
22 
assoc_fold.ML fold numerals in nested products 

23 
cancel_numerals.ML cancel common coefficients in balanced expressions 

4623  24 
cancel_factor.ML cancel common constant factor 
25 
cancel_sums.ML cancel common summands 

8870  26 
combine_numerals.ML combine coefficients in expressions 
27 
fast_lin_arith.ML generic linear arithmetic package 