NameDateSize

..25-Jul-201916

Arith/H25-Jul-20199

blast.MLH A D25-Jul-201954.3 KiB

clasimp.MLH A D25-Jul-20196.9 KiB

classical.MLH A D25-Jul-201937.5 KiB

hypsubst.MLH A D25-Jul-201912.6 KiB

order.MLH A D25-Jul-201957.9 KiB

quantifier1.MLH A D25-Jul-20197.7 KiB

quasi.MLH A D25-Jul-201925.7 KiB

READMEH A D25-Jul-2019968

splitter.MLH A D25-Jul-201918.3 KiB

trancl.MLH A D25-Jul-201922 KiB

typedsimp.MLH A D25-Jul-20194.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