src/Provers/README
author wenzelm
Wed May 21 17:13:00 1997 +0200 (1997-05-21)
changeset 3279 815ef5848324
parent 195 1315ce07f515
child 4289 5c1bfefd39b7
permissions -rw-r--r--
tuned all READMEs;
clasohm@0
     1
			Provers
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@3279
     8
blast.ML          -- generic tableau prover with proof reconstruction
wenzelm@3279
     9
classical.ML      -- theorem prover for classical logics
wenzelm@3279
    10
genelim.ML        -- bits and pieces for deriving elimination rules
wenzelm@3279
    11
hypsubst.ML       -- tactic to substitute in the hypotheses
wenzelm@3279
    12
ind.ML            -- a simple induction package
wenzelm@3279
    13
nat_transitive.ML -- simple package for inequalities over nat
wenzelm@3279
    14
simp.ML           -- powerful but slow simplifier
wenzelm@3279
    15
simplifier.ML     -- fast simplifier
wenzelm@3279
    16
splitter.ML       -- performs case splits for simplifier.ML
wenzelm@3279
    17
typedsimp.ML      -- basic simplifier for explicitly typed logics