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

src/Provers/README

author | wenzelm |

Thu, 12 Feb 1998 15:43:50 +0100 | |

changeset 4623 | e6ada440a383 |

parent 4289 | 5c1bfefd39b7 |

child 4654 | dbeae12ada20 |

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

updated;

Provers: generic theorem proving tools 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. blast.ML generic tableau prover with proof reconstruction classical.ML theorem prover for classical logics genelim.ML bits and pieces for deriving elimination rules hypsubst.ML tactic to substitute in the hypotheses ind.ML a simple induction package quantifier1.ML simplification procedures for "1 point rules" simp.ML powerful but slow simplifier simplifier.ML fast simplifier splitter.ML performs case splits for simplifier.ML typedsimp.ML basic simplifier for explicitly typed logics directory Arith: cancel_factor.ML cancel common constant factor cancel_sums.ML cancel common summands nat_transitive.ML simple package for inequalities over nat