src/Provers/README
author wenzelm
Wed Apr 04 00:11:03 2007 +0200 (2007-04-04)
changeset 22578 b0eb5652f210
parent 16019 0e1405402d53
child 30159 7b55b6b5c0c2
permissions -rw-r--r--
removed obsolete sign_of/sign_of_thm;
     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   linorder.ML		transitivity reasoner for linear (total) orders
    15   quantifier1.ML	simplification procedures for "1 point rules"
    16   simp.ML               powerful but slow simplifier
    17   split_paired_all.ML	turn surjective pairing into split rule
    18   splitter.ML           performs case splits for simplifier
    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