src/Provers/README
author blanchet
Tue, 07 Dec 2010 11:56:01 +0100
changeset 41051 2ed1b971fc20
parent 38052 04a8de29e8f7
permissions -rw-r--r--
give the inner timeout mechanism a chance, since it gives more precise information to the user
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
30159
7b55b6b5c0c2 some updates on ancient README;
wenzelm
parents: 16019
diff changeset
     5
certain form are derivable.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
     7
  blast.ML              generic tableau prover with proof reconstruction
4654
dbeae12ada20 added clasimp.ML;
wenzelm
parents: 4623
diff changeset
     8
  clasimp.ML		combination of classical reasoner and simplifier
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
     9
  classical.ML          theorem prover for classical logics
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    10
  hypsubst.ML           tactic to substitute in the hypotheses
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    11
  quantifier1.ML	simplification procedures for "1 point rules"
16019
0e1405402d53 Simplifier already setup in Pure;
wenzelm
parents: 13736
diff changeset
    12
  splitter.ML           performs case splits for simplifier
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    13
  typedsimp.ML          basic simplifier for explicitly typed logics
4289
wenzelm
parents: 3279
diff changeset
    14
wenzelm
parents: 3279
diff changeset
    15
directory Arith:
8870
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    16
  assoc_fold.ML		fold numerals in nested products
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    17
  cancel_numerals.ML	cancel common coefficients in balanced expressions
4623
e6ada440a383 updated;
wenzelm
parents: 4289
diff changeset
    18
  cancel_sums.ML	cancel common summands
8870
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    19
  combine_numerals.ML	combine coefficients in expressions
e900a58cafe4 updated
paulson
parents: 5897
diff changeset
    20
  fast_lin_arith.ML	generic linear arithmetic package