summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Provers/README

author | wenzelm |

Thu Dec 07 00:42:04 2006 +0100 (2006-12-07) | |

changeset 21687 | f689f729afab |

parent 16019 | 0e1405402d53 |

child 30159 | 7b55b6b5c0c2 |

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

reorganized structure Goal vs. Tactic;

1 Provers: generic theorem proving tools

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. Some of these are documented in the

6 Reference Manual.

8 blast.ML generic tableau prover with proof reconstruction

9 clasimp.ML combination of classical reasoner and simplifier

10 classical.ML theorem prover for classical logics

11 hypsubst.ML tactic to substitute in the hypotheses

12 ind.ML a simple induction package

13 induct_method.ML proof by cases and induction on sets and types (Isar)

14 linorder.ML transitivity reasoner for linear (total) orders

15 quantifier1.ML simplification procedures for "1 point rules"

16 simp.ML powerful but slow simplifier

17 split_paired_all.ML turn surjective pairing into split rule

18 splitter.ML performs case splits for simplifier

19 typedsimp.ML basic simplifier for explicitly typed logics

21 directory Arith:

22 abel_cancel.ML cancel complementary terms in sums of Abelian groups

23 assoc_fold.ML fold numerals in nested products

24 cancel_numerals.ML cancel common coefficients in balanced expressions

25 cancel_factor.ML cancel common constant factor

26 cancel_sums.ML cancel common summands

27 combine_numerals.ML combine coefficients in expressions

28 fast_lin_arith.ML generic linear arithmetic package