src/Provers/README
 author wenzelm Tue, 24 Jul 2012 21:36:53 +0200 changeset 48487 94a9650f79fb parent 38052 04a8de29e8f7 permissions -rw-r--r--
tuned order;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
 4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset ` 1` ``` Provers: generic theorem proving tools ``` 0 a5a9c433f639 Initial revision clasohm parents: diff changeset ` 2` a5a9c433f639 Initial revision clasohm parents: diff changeset ` 3` ```This directory contains ML sources of generic theorem proving tools. ``` a5a9c433f639 Initial revision clasohm parents: diff changeset ` 4` ```Typically, they can be applied to various logics, provided rules of a ``` 30159 7b55b6b5c0c2 some updates on ancient README; wenzelm parents: 16019 diff changeset ` 5` ```certain form are derivable. ``` 0 a5a9c433f639 Initial revision clasohm parents: diff changeset ` 6` 4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset ` 7` ``` blast.ML generic tableau prover with proof reconstruction ``` 4654 dbeae12ada20 added clasimp.ML; wenzelm parents: 4623 diff changeset ` 8` ``` clasimp.ML combination of classical reasoner and simplifier ``` 4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset ` 9` ``` classical.ML theorem prover for classical logics ``` e6ada440a383 updated; wenzelm parents: 4289 diff changeset ` 10` ``` hypsubst.ML tactic to substitute in the hypotheses ``` e6ada440a383 updated; wenzelm parents: 4289 diff changeset ` 11` ``` quantifier1.ML simplification procedures for "1 point rules" ``` 16019 0e1405402d53 Simplifier already setup in Pure; wenzelm parents: 13736 diff changeset ` 12` ``` splitter.ML performs case splits for simplifier ``` 4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset ` 13` ``` typedsimp.ML basic simplifier for explicitly typed logics ``` 4289 5c1bfefd39b7 tuned; wenzelm parents: 3279 diff changeset ` 14` 5c1bfefd39b7 tuned; wenzelm parents: 3279 diff changeset ` 15` ```directory Arith: ``` 8870 e900a58cafe4 updated paulson parents: 5897 diff changeset ` 16` ``` assoc_fold.ML fold numerals in nested products ``` e900a58cafe4 updated paulson parents: 5897 diff changeset ` 17` ``` cancel_numerals.ML cancel common coefficients in balanced expressions ``` 4623 e6ada440a383 updated; wenzelm parents: 4289 diff changeset ` 18` ``` cancel_sums.ML cancel common summands ``` 8870 e900a58cafe4 updated paulson parents: 5897 diff changeset ` 19` ``` combine_numerals.ML combine coefficients in expressions ``` e900a58cafe4 updated paulson parents: 5897 diff changeset ` 20` ``` fast_lin_arith.ML generic linear arithmetic package ```