src/Provers/README
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 30159 7b55b6b5c0c2
child 38052 04a8de29e8f7
permissions -rw-r--r--
modernized structure Object_Logic;
     1                  Provers: generic theorem proving tools
     2 
     3 This directory contains ML sources of generic theorem proving tools.
     4 Typically, they can be applied to various logics, provided rules of a
     5 certain form are derivable.
     6 
     7   blast.ML              generic tableau prover with proof reconstruction
     8   clasimp.ML		combination of classical reasoner and simplifier
     9   classical.ML          theorem prover for classical logics
    10   hypsubst.ML           tactic to substitute in the hypotheses
    11   quantifier1.ML	simplification procedures for "1 point rules"
    12   splitter.ML           performs case splits for simplifier
    13   typedsimp.ML          basic simplifier for explicitly typed logics
    14 
    15 directory Arith:
    16   abel_cancel.ML	cancel complementary terms in sums of Abelian groups
    17   assoc_fold.ML		fold numerals in nested products
    18   cancel_numerals.ML	cancel common coefficients in balanced expressions
    19   cancel_factor.ML	cancel common constant factor
    20   cancel_sums.ML	cancel common summands
    21   combine_numerals.ML	combine coefficients in expressions
    22   fast_lin_arith.ML	generic linear arithmetic package