src/Provers/README
author wenzelm
Thu Feb 12 15:43:50 1998 +0100 (1998-02-12)
changeset 4623 e6ada440a383
parent 4289 5c1bfefd39b7
child 4654 dbeae12ada20
permissions -rw-r--r--
updated;
     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   classical.ML          theorem prover for classical logics
    10   genelim.ML            bits and pieces for deriving elimination rules
    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
    16   splitter.ML           performs case splits for simplifier.ML
    17   typedsimp.ML          basic simplifier for explicitly typed logics
    18 
    19 directory Arith:
    20   cancel_factor.ML	cancel common constant factor
    21   cancel_sums.ML	cancel common summands
    22   nat_transitive.ML	simple package for inequalities over nat