src/Provers/README
author paulson
Fri, 12 May 2000 15:21:58 +0200
changeset 8870 e900a58cafe4
parent 5897 b3548f939dd2
child 11840 54fe56353704
permissions -rw-r--r--
updated
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
     1
                 Provers: generic theorem proving tools
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
This directory contains ML sources of generic theorem proving tools.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
Typically, they can be applied to various logics, provided rules of a
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
     5
certain form are derivable.  Some of these are documented in the
195
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
     6
Reference Manual.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
     8
  blast.ML              generic tableau prover with proof reconstruction
4654
dbeae12ada20 added clasimp.ML;
wenzelm
parents: 4623
diff changeset
     9
  clasimp.ML		combination of classical reasoner and simplifier
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    10
  classical.ML          theorem prover for classical logics
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    11
  hypsubst.ML           tactic to substitute in the hypotheses
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    12
  ind.ML                a simple induction package
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    13
  quantifier1.ML	simplification procedures for "1 point rules"
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    14
  simp.ML               powerful but slow simplifier
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    15
  simplifier.ML         fast simplifier
5680
4f526bcd3a68 split_paired_all.ML: turn surjective pairing into split rule;
wenzelm
parents: 4654
diff changeset
    16
  split_paired_all.ML	turn surjective pairing into split rule
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    17
  splitter.ML           performs case splits for simplifier.ML
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    18
  typedsimp.ML          basic simplifier for explicitly typed logics
4289
wenzelm
parents: 3279
diff changeset
    19
wenzelm
parents: 3279
diff changeset
    20
directory Arith:
8870
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    21
  abel_cancel.ML	cancel complementary terms in sums of Abelian groups
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    22
  assoc_fold.ML		fold numerals in nested products
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    23
  cancel_numerals.ML	cancel common coefficients in balanced expressions
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    24
  cancel_factor.ML	cancel common constant factor
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    25
  cancel_sums.ML	cancel common summands
8870
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    26
  combine_numerals.ML	combine coefficients in expressions
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    27
  fast_lin_arith.ML	generic linear arithmetic package