summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/Provers/README

changeset 30159 | 7b55b6b5c0c2 |

parent 16019 | 0e1405402d53 |

child 38052 | 04a8de29e8f7 |

--- a/src/Provers/README Fri Feb 27 19:05:46 2009 -0800 +++ b/src/Provers/README Sat Feb 28 13:54:47 2009 +0100 @@ -2,19 +2,13 @@ This directory contains ML sources of generic theorem proving tools. Typically, they can be applied to various logics, provided rules of a -certain form are derivable. Some of these are documented in the -Reference Manual. +certain form are derivable. blast.ML generic tableau prover with proof reconstruction clasimp.ML combination of classical reasoner and simplifier classical.ML theorem prover for classical logics hypsubst.ML tactic to substitute in the hypotheses - ind.ML a simple induction package - induct_method.ML proof by cases and induction on sets and types (Isar) - linorder.ML transitivity reasoner for linear (total) orders quantifier1.ML simplification procedures for "1 point rules" - simp.ML powerful but slow simplifier - split_paired_all.ML turn surjective pairing into split rule splitter.ML performs case splits for simplifier typedsimp.ML basic simplifier for explicitly typed logics