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;
wenzelm@4623
     1
                 Provers: generic theorem proving tools
clasohm@0
     2
clasohm@0
     3
This directory contains ML sources of generic theorem proving tools.
clasohm@0
     4
Typically, they can be applied to various logics, provided rules of a
wenzelm@3279
     5
certain form are derivable.  Some of these are documented in the
lcp@195
     6
Reference Manual.
clasohm@0
     7
wenzelm@4623
     8
  blast.ML              generic tableau prover with proof reconstruction
wenzelm@4623
     9
  classical.ML          theorem prover for classical logics
wenzelm@4623
    10
  genelim.ML            bits and pieces for deriving elimination rules
wenzelm@4623
    11
  hypsubst.ML           tactic to substitute in the hypotheses
wenzelm@4623
    12
  ind.ML                a simple induction package
wenzelm@4623
    13
  quantifier1.ML	simplification procedures for "1 point rules"
wenzelm@4623
    14
  simp.ML               powerful but slow simplifier
wenzelm@4623
    15
  simplifier.ML         fast simplifier
wenzelm@4623
    16
  splitter.ML           performs case splits for simplifier.ML
wenzelm@4623
    17
  typedsimp.ML          basic simplifier for explicitly typed logics
wenzelm@4289
    18
wenzelm@4289
    19
directory Arith:
wenzelm@4623
    20
  cancel_factor.ML	cancel common constant factor
wenzelm@4623
    21
  cancel_sums.ML	cancel common summands
wenzelm@4623
    22
  nat_transitive.ML	simple package for inequalities over nat