Name | Date | Size | ||
---|---|---|---|---|
.. | 25-Jul-2019 | 16 | ||
Arith/ | H | 25-Jul-2019 | 9 | |
blast.ML | H A D | 25-Jul-2019 | 54.3 KiB | |
clasimp.ML | H A D | 25-Jul-2019 | 6.9 KiB | |
classical.ML | H A D | 25-Jul-2019 | 37.5 KiB | |
hypsubst.ML | H A D | 25-Jul-2019 | 12.6 KiB | |
order.ML | H A D | 25-Jul-2019 | 57.9 KiB | |
quantifier1.ML | H A D | 25-Jul-2019 | 7.7 KiB | |
quasi.ML | H A D | 25-Jul-2019 | 25.7 KiB | |
README | H A D | 25-Jul-2019 | 968 | |
splitter.ML | H A D | 25-Jul-2019 | 18.3 KiB | |
trancl.ML | H A D | 25-Jul-2019 | 22 KiB | |
typedsimp.ML | H A D | 25-Jul-2019 | 4.7 KiB |
README
1 Provers: generic theorem proving tools 2 3This directory contains ML sources of generic theorem proving tools. 4Typically, they can be applied to various logics, provided rules of a 5certain form are derivable. 6 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 14 15directory 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 21