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
genelim.ML bits and pieces for deriving elimination rules
hypsubst.ML tactic to substitute in the hypotheses
ind.ML a simple induction package
quantifier1.ML simplification procedures for "1 point rules"
simp.ML powerful but slow simplifier
simplifier.ML fast simplifier
split_paired_all.ML turn surjective pairing into split rule
splitter.ML performs case splits for simplifier.ML
typedsimp.ML basic simplifier for explicitly typed logics
directory Arith:
cancel_factor.ML cancel common constant factor
cancel_sums.ML cancel common summands
nat_transitive.ML simple package for inequalities over nat