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

src/Provers/README

author | wenzelm |

Thu Feb 12 15:43:50 1998 +0100 (1998-02-12) | |

changeset 4623 | e6ada440a383 |

parent 4289 | 5c1bfefd39b7 |

child 4654 | dbeae12ada20 |

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

updated;

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 classical.ML theorem prover for classical logics

10 genelim.ML bits and pieces for deriving elimination rules

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 splitter.ML performs case splits for simplifier.ML

17 typedsimp.ML basic simplifier for explicitly typed logics

19 directory Arith:

20 cancel_factor.ML cancel common constant factor

21 cancel_sums.ML cancel common summands

22 nat_transitive.ML simple package for inequalities over nat