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