src/Provers/README
author nipkow
Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago)
changeset 13157 4a4599f78f18
parent 11840 54fe56353704
child 13735 7de9342aca7a
permissions -rw-r--r--
allowed more general split rules to cope with div/mod 2
     1                  Provers: generic theorem proving tools
     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
     5 certain form are derivable.  Some of these are documented in the
     6 Reference Manual.
     7 
     8   blast.ML              generic tableau prover with proof reconstruction
     9   clasimp.ML		combination of classical reasoner and simplifier
    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   induct_method.ML      proof by cases and induction on sets and types (Isar)
    14   quantifier1.ML	simplification procedures for "1 point rules"
    15   simp.ML               powerful but slow simplifier
    16   simplifier.ML         fast simplifier
    17   split_paired_all.ML	turn surjective pairing into split rule
    18   splitter.ML           performs case splits for simplifier.ML
    19   typedsimp.ML          basic simplifier for explicitly typed logics
    20 
    21 directory Arith:
    22   abel_cancel.ML	cancel complementary terms in sums of Abelian groups
    23   assoc_fold.ML		fold numerals in nested products
    24   cancel_numerals.ML	cancel common coefficients in balanced expressions
    25   cancel_factor.ML	cancel common constant factor
    26   cancel_sums.ML	cancel common summands
    27   combine_numerals.ML	combine coefficients in expressions
    28   fast_lin_arith.ML	generic linear arithmetic package