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

src/Provers/README

author | wenzelm |

Sun Mar 07 12:19:47 2010 +0100 (2010-03-07) | |

changeset 35625 | 9c818cab0dd0 |

parent 30159 | 7b55b6b5c0c2 |

child 38052 | 04a8de29e8f7 |

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

modernized structure Object_Logic;

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.

7 blast.ML generic tableau prover with proof reconstruction

8 clasimp.ML combination of classical reasoner and simplifier

9 classical.ML theorem prover for classical logics

10 hypsubst.ML tactic to substitute in the hypotheses

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

12 splitter.ML performs case splits for simplifier

13 typedsimp.ML basic simplifier for explicitly typed logics

15 directory Arith:

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

17 assoc_fold.ML fold numerals in nested products

18 cancel_numerals.ML cancel common coefficients in balanced expressions

19 cancel_factor.ML cancel common constant factor

20 cancel_sums.ML cancel common summands

21 combine_numerals.ML combine coefficients in expressions

22 fast_lin_arith.ML generic linear arithmetic package