wenzelm@4623: Provers: generic theorem proving tools
clasohm@0:
clasohm@0: This directory contains ML sources of generic theorem proving tools.
clasohm@0: Typically, they can be applied to various logics, provided rules of a
wenzelm@3279: certain form are derivable. Some of these are documented in the
lcp@195: Reference Manual.
clasohm@0:
wenzelm@4623: blast.ML generic tableau prover with proof reconstruction
wenzelm@4654: clasimp.ML combination of classical reasoner and simplifier
wenzelm@4623: classical.ML theorem prover for classical logics
wenzelm@4623: hypsubst.ML tactic to substitute in the hypotheses
wenzelm@4623: ind.ML a simple induction package
wenzelm@11840: induct_method.ML proof by cases and induction on sets and types (Isar)
ballarin@13736: linorder.ML transitivity reasoner for linear (total) orders
wenzelm@4623: quantifier1.ML simplification procedures for "1 point rules"
wenzelm@4623: simp.ML powerful but slow simplifier
wenzelm@5680: split_paired_all.ML turn surjective pairing into split rule
wenzelm@16019: splitter.ML performs case splits for simplifier
wenzelm@4623: typedsimp.ML basic simplifier for explicitly typed logics
wenzelm@4289:
wenzelm@4289: directory Arith:
paulson@8870: abel_cancel.ML cancel complementary terms in sums of Abelian groups
paulson@8870: assoc_fold.ML fold numerals in nested products
paulson@8870: cancel_numerals.ML cancel common coefficients in balanced expressions
wenzelm@4623: cancel_factor.ML cancel common constant factor
wenzelm@4623: cancel_sums.ML cancel common summands
paulson@8870: combine_numerals.ML combine coefficients in expressions
paulson@8870: fast_lin_arith.ML generic linear arithmetic package