src/Provers/README
author wenzelm
Sun, 30 Nov 2008 14:43:29 +0100
changeset 28917 20f43e0e0958
parent 16019 0e1405402d53
child 30159 7b55b6b5c0c2
permissions -rw-r--r--
tuned;

                 Provers: generic theorem proving tools

This directory contains ML sources of generic theorem proving tools.
Typically, they can be applied to various logics, provided rules of a
certain form are derivable.  Some of these are documented in the
Reference Manual.

  blast.ML              generic tableau prover with proof reconstruction
  clasimp.ML		combination of classical reasoner and simplifier
  classical.ML          theorem prover for classical logics
  hypsubst.ML           tactic to substitute in the hypotheses
  ind.ML                a simple induction package
  induct_method.ML      proof by cases and induction on sets and types (Isar)
  linorder.ML		transitivity reasoner for linear (total) orders
  quantifier1.ML	simplification procedures for "1 point rules"
  simp.ML               powerful but slow simplifier
  split_paired_all.ML	turn surjective pairing into split rule
  splitter.ML           performs case splits for simplifier
  typedsimp.ML          basic simplifier for explicitly typed logics

directory Arith:
  abel_cancel.ML	cancel complementary terms in sums of Abelian groups
  assoc_fold.ML		fold numerals in nested products
  cancel_numerals.ML	cancel common coefficients in balanced expressions
  cancel_factor.ML	cancel common constant factor
  cancel_sums.ML	cancel common summands
  combine_numerals.ML	combine coefficients in expressions
  fast_lin_arith.ML	generic linear arithmetic package