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

src/Provers/README

author | wenzelm |

Thu Jul 27 11:44:29 2000 +0200 (2000-07-27 ago) | |

changeset 9449 | 2f814053a6cc |

parent 8870 | e900a58cafe4 |

child 11840 | 54fe56353704 |

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

intro_elim_tac: bimatch_from;

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

14 simp.ML powerful but slow simplifier

15 simplifier.ML fast simplifier

16 split_paired_all.ML turn surjective pairing into split rule

17 splitter.ML performs case splits for simplifier.ML

18 typedsimp.ML basic simplifier for explicitly typed logics

20 directory Arith:

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

22 assoc_fold.ML fold numerals in nested products

23 cancel_numerals.ML cancel common coefficients in balanced expressions

24 cancel_factor.ML cancel common constant factor

25 cancel_sums.ML cancel common summands

26 combine_numerals.ML combine coefficients in expressions

27 fast_lin_arith.ML generic linear arithmetic package