summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Provers/README

author | ballarin |

Thu, 28 Nov 2002 10:50:42 +0100 | |

changeset 13735 | 7de9342aca7a |

parent 11840 | 54fe56353704 |

child 13736 | 6ea0e7c43c4f |

permissions | -rw-r--r-- |

HOL-Algebra partially ported to Isar.

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) 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 trans.ML transitivity reasoner for linear (total) orders 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