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

src/Provers/README

author | Manuel Eberl <eberlm@in.tum.de> |

Wed, 07 Apr 2021 11:05:00 +0200 | |

changeset 73791 | 16a2b7f582fa |

parent 38052 | 04a8de29e8f7 |

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

fixed problematic addition operation in the 'approximation' package (previous version used much too high precision sometimes)

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. 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 quantifier1.ML simplification procedures for "1 point rules" splitter.ML performs case splits for simplifier typedsimp.ML basic simplifier for explicitly typed logics directory Arith: assoc_fold.ML fold numerals in nested products cancel_numerals.ML cancel common coefficients in balanced expressions cancel_sums.ML cancel common summands combine_numerals.ML combine coefficients in expressions fast_lin_arith.ML generic linear arithmetic package