author  ballarin 
Thu, 28 Nov 2002 10:50:42 +0100  
changeset 13735  7de9342aca7a 
parent 11840  54fe56353704 
child 13736  6ea0e7c43c4f 
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 

11840
54fe56353704
induct_method.ML  proof by cases and induction on sets and types (Isar);
wenzelm
parents:
8870
diff
changeset

13 
induct_method.ML proof by cases and induction on sets and types (Isar) 
4623  14 
quantifier1.ML simplification procedures for "1 point rules" 
15 
simp.ML powerful but slow simplifier 

16 
simplifier.ML fast simplifier 

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

17 
split_paired_all.ML turn surjective pairing into split rule 
4623  18 
splitter.ML performs case splits for simplifier.ML 
13735  19 
trans.ML transitivity reasoner for linear (total) orders 
4623  20 
typedsimp.ML basic simplifier for explicitly typed logics 
4289  21 

22 
directory Arith: 

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

25 
cancel_numerals.ML cancel common coefficients in balanced expressions 

4623  26 
cancel_factor.ML cancel common constant factor 
27 
cancel_sums.ML cancel common summands 

8870  28 
combine_numerals.ML combine coefficients in expressions 
29 
fast_lin_arith.ML generic linear arithmetic package 