src/Provers/README
author wenzelm
Wed Nov 26 16:41:25 1997 +0100 (1997-11-26)
changeset 4289 5c1bfefd39b7
parent 3279 815ef5848324
child 4623 e6ada440a383
permissions -rw-r--r--
tuned;
wenzelm@4289
     1
wenzelm@4289
     2
                        Provers
clasohm@0
     3
clasohm@0
     4
This directory contains ML sources of generic theorem proving tools.
clasohm@0
     5
Typically, they can be applied to various logics, provided rules of a
wenzelm@3279
     6
certain form are derivable.  Some of these are documented in the
lcp@195
     7
Reference Manual.
clasohm@0
     8
wenzelm@4289
     9
blast.ML                -- generic tableau prover with proof reconstruction
wenzelm@4289
    10
classical.ML            -- theorem prover for classical logics
wenzelm@4289
    11
genelim.ML              -- bits and pieces for deriving elimination rules
wenzelm@4289
    12
hypsubst.ML             -- tactic to substitute in the hypotheses
wenzelm@4289
    13
ind.ML                  -- a simple induction package
wenzelm@4289
    14
simp.ML                 -- powerful but slow simplifier
wenzelm@4289
    15
simplifier.ML           -- fast simplifier
wenzelm@4289
    16
splitter.ML             -- performs case splits for simplifier.ML
wenzelm@4289
    17
typedsimp.ML            -- basic simplifier for explicitly typed logics
wenzelm@4289
    18
wenzelm@4289
    19
directory Arith:
wenzelm@4289
    20
  nat_transitive.ML     -- simple package for inequalities over nat
wenzelm@4289
    21
wenzelm@4289
    22
wenzelm@4289
    23
$Id$