src/Provers/README
author wenzelm
Wed, 15 Oct 1997 15:12:59 +0200
changeset 3872 a5839ecee7b8
parent 3279 815ef5848324
child 4289 5c1bfefd39b7
permissions -rw-r--r--
tuned; prepare ext;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
			Provers
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
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
     8
blast.ML          -- generic tableau prover with proof reconstruction
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
     9
classical.ML      -- theorem prover for classical logics
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
    10
genelim.ML        -- bits and pieces for deriving elimination rules
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
    11
hypsubst.ML       -- tactic to substitute in the hypotheses
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
    12
ind.ML            -- a simple induction package
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
    13
nat_transitive.ML -- simple package for inequalities over nat
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
    14
simp.ML           -- powerful but slow simplifier
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
    15
simplifier.ML     -- fast simplifier
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
    16
splitter.ML       -- performs case splits for simplifier.ML
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
    17
typedsimp.ML      -- basic simplifier for explicitly typed logics