src/Provers/README
changeset 4623 e6ada440a383
parent 4289 5c1bfefd39b7
child 4654 dbeae12ada20
equal deleted inserted replaced
4622:85aae356570c 4623:e6ada440a383
     1 
     1                  Provers: generic theorem proving tools
     2                         Provers
       
     3 
     2 
     4 This directory contains ML sources of generic theorem proving tools.
     3 This directory contains ML sources of generic theorem proving tools.
     5 Typically, they can be applied to various logics, provided rules of a
     4 Typically, they can be applied to various logics, provided rules of a
     6 certain form are derivable.  Some of these are documented in the
     5 certain form are derivable.  Some of these are documented in the
     7 Reference Manual.
     6 Reference Manual.
     8 
     7 
     9 blast.ML                -- generic tableau prover with proof reconstruction
     8   blast.ML              generic tableau prover with proof reconstruction
    10 classical.ML            -- theorem prover for classical logics
     9   classical.ML          theorem prover for classical logics
    11 genelim.ML              -- bits and pieces for deriving elimination rules
    10   genelim.ML            bits and pieces for deriving elimination rules
    12 hypsubst.ML             -- tactic to substitute in the hypotheses
    11   hypsubst.ML           tactic to substitute in the hypotheses
    13 ind.ML                  -- a simple induction package
    12   ind.ML                a simple induction package
    14 simp.ML                 -- powerful but slow simplifier
    13   quantifier1.ML	simplification procedures for "1 point rules"
    15 simplifier.ML           -- fast simplifier
    14   simp.ML               powerful but slow simplifier
    16 splitter.ML             -- performs case splits for simplifier.ML
    15   simplifier.ML         fast simplifier
    17 typedsimp.ML            -- basic simplifier for explicitly typed logics
    16   splitter.ML           performs case splits for simplifier.ML
       
    17   typedsimp.ML          basic simplifier for explicitly typed logics
    18 
    18 
    19 directory Arith:
    19 directory Arith:
    20   nat_transitive.ML     -- simple package for inequalities over nat
    20   cancel_factor.ML	cancel common constant factor
    21 
    21   cancel_sums.ML	cancel common summands
    22 
    22   nat_transitive.ML	simple package for inequalities over nat
    23 $Id$