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

src/Provers/README

author | nipkow |

Fri May 17 11:25:07 2002 +0200 (2002-05-17 ago) | |

changeset 13157 | 4a4599f78f18 |

parent 11840 | 54fe56353704 |

child 13735 | 7de9342aca7a |

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

allowed more general split rules to cope with div/mod 2

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 quantifier1.ML simplification procedures for "1 point rules"

15 simp.ML powerful but slow simplifier

16 simplifier.ML fast simplifier

17 split_paired_all.ML turn surjective pairing into split rule

18 splitter.ML performs case splits for simplifier.ML

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