src/Provers/README
author paulson
Sat, 10 Jan 1998 17:59:32 +0100
changeset 4552 bb8ff763c93d
parent 4289 5c1bfefd39b7
child 4623 e6ada440a383
permissions -rw-r--r--
Simplified proofs by omitting PA = {|XA, ...|} from RA2
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4289
wenzelm
parents: 3279
diff changeset
     1
wenzelm
parents: 3279
diff changeset
     2
                        Provers
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
This directory contains ML sources of generic theorem proving tools.
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
Typically, they can be applied to various logics, provided rules of a
3279
815ef5848324 tuned all READMEs;
wenzelm
parents: 195
diff changeset
     6
certain form are derivable.  Some of these are documented in the
195
1315ce07f515 added mention of simplifier, splitter, hypsubst
lcp
parents: 0
diff changeset
     7
Reference Manual.
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
4289
wenzelm
parents: 3279
diff changeset
     9
blast.ML                -- generic tableau prover with proof reconstruction
wenzelm
parents: 3279
diff changeset
    10
classical.ML            -- theorem prover for classical logics
wenzelm
parents: 3279
diff changeset
    11
genelim.ML              -- bits and pieces for deriving elimination rules
wenzelm
parents: 3279
diff changeset
    12
hypsubst.ML             -- tactic to substitute in the hypotheses
wenzelm
parents: 3279
diff changeset
    13
ind.ML                  -- a simple induction package
wenzelm
parents: 3279
diff changeset
    14
simp.ML                 -- powerful but slow simplifier
wenzelm
parents: 3279
diff changeset
    15
simplifier.ML           -- fast simplifier
wenzelm
parents: 3279
diff changeset
    16
splitter.ML             -- performs case splits for simplifier.ML
wenzelm
parents: 3279
diff changeset
    17
typedsimp.ML            -- basic simplifier for explicitly typed logics
wenzelm
parents: 3279
diff changeset
    18
wenzelm
parents: 3279
diff changeset
    19
directory Arith:
wenzelm
parents: 3279
diff changeset
    20
  nat_transitive.ML     -- simple package for inequalities over nat
wenzelm
parents: 3279
diff changeset
    21
wenzelm
parents: 3279
diff changeset
    22
wenzelm
parents: 3279
diff changeset
    23
$Id$