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

src/Provers/README

author | wenzelm |

Mon Mar 25 16:45:08 2019 +0100 (3 months ago) | |

changeset 69980 | f2e3adfd916f |

parent 38052 | 04a8de29e8f7 |

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

tuned signature;

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 assoc_fold.ML fold numerals in nested products

17 cancel_numerals.ML cancel common coefficients in balanced expressions

18 cancel_sums.ML cancel common summands

19 combine_numerals.ML combine coefficients in expressions

20 fast_lin_arith.ML generic linear arithmetic package