src/Provers/README
author ballarin
Thu Nov 28 15:44:34 2002 +0100 (2002-11-28)
changeset 13736 6ea0e7c43c4f
parent 13735 7de9342aca7a
child 16019 0e1405402d53
permissions -rw-r--r--
Transitivity reasoner renamed to linorder.ML. README 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@4654
     9
  clasimp.ML		combination of classical reasoner and simplifier
wenzelm@4623
    10
  classical.ML          theorem prover for classical logics
wenzelm@4623
    11
  hypsubst.ML           tactic to substitute in the hypotheses
wenzelm@4623
    12
  ind.ML                a simple induction package
wenzelm@11840
    13
  induct_method.ML      proof by cases and induction on sets and types (Isar)
ballarin@13736
    14
  linorder.ML		transitivity reasoner for linear (total) orders
wenzelm@4623
    15
  quantifier1.ML	simplification procedures for "1 point rules"
wenzelm@4623
    16
  simp.ML               powerful but slow simplifier
wenzelm@4623
    17
  simplifier.ML         fast simplifier
wenzelm@5680
    18
  split_paired_all.ML	turn surjective pairing into split rule
wenzelm@4623
    19
  splitter.ML           performs case splits for simplifier.ML
wenzelm@4623
    20
  typedsimp.ML          basic simplifier for explicitly typed logics
wenzelm@4289
    21
wenzelm@4289
    22
directory Arith:
paulson@8870
    23
  abel_cancel.ML	cancel complementary terms in sums of Abelian groups
paulson@8870
    24
  assoc_fold.ML		fold numerals in nested products
paulson@8870
    25
  cancel_numerals.ML	cancel common coefficients in balanced expressions
wenzelm@4623
    26
  cancel_factor.ML	cancel common constant factor
wenzelm@4623
    27
  cancel_sums.ML	cancel common summands
paulson@8870
    28
  combine_numerals.ML	combine coefficients in expressions
paulson@8870
    29
  fast_lin_arith.ML	generic linear arithmetic package