src/Provers/README
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 38052 04a8de29e8f7
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
wenzelm@4623
     1
                 Provers: generic theorem proving tools
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@30159
     5
certain form are derivable.
clasohm@0
     6
wenzelm@4623
     7
  blast.ML              generic tableau prover with proof reconstruction
wenzelm@4654
     8
  clasimp.ML		combination of classical reasoner and simplifier
wenzelm@4623
     9
  classical.ML          theorem prover for classical logics
wenzelm@4623
    10
  hypsubst.ML           tactic to substitute in the hypotheses
wenzelm@4623
    11
  quantifier1.ML	simplification procedures for "1 point rules"
wenzelm@16019
    12
  splitter.ML           performs case splits for simplifier
wenzelm@4623
    13
  typedsimp.ML          basic simplifier for explicitly typed logics
wenzelm@4289
    14
wenzelm@4289
    15
directory Arith:
paulson@8870
    16
  assoc_fold.ML		fold numerals in nested products
paulson@8870
    17
  cancel_numerals.ML	cancel common coefficients in balanced expressions
wenzelm@4623
    18
  cancel_sums.ML	cancel common summands
paulson@8870
    19
  combine_numerals.ML	combine coefficients in expressions
paulson@8870
    20
  fast_lin_arith.ML	generic linear arithmetic package