src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
2011-05-12 blanchet 2011-05-12 renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
2011-05-12 blanchet 2011-05-12 remove unused parameter
2011-05-12 blanchet 2011-05-12 reduced penalty associated with existential quantifiers
2011-05-12 blanchet 2011-05-12 fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
2011-05-12 blanchet 2011-05-12 improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
2011-05-12 blanchet 2011-05-12 tune whitespace
2011-05-12 blanchet 2011-05-12 added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
2011-05-12 blanchet 2011-05-12 allow each slice to have its own type system
2011-05-12 blanchet 2011-05-12 renamed type systems for more consistency
2011-05-06 blanchet 2011-05-06 allow each prover to specify its own formula kind for symbols occurring in the conjecture
2011-05-05 blanchet 2011-05-05 no lies in debug output (e.g. "slice 2 of 1")
2011-05-04 blanchet 2011-05-04 renamed "many_typed" to "simple" (as in simple types)
2011-05-04 blanchet 2011-05-04 added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
2011-05-03 blanchet 2011-05-03 fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
2011-05-03 blanchet 2011-05-03 no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
2011-05-03 blanchet 2011-05-03 replaced some Unsynchronized.refs with Config.Ts
2011-05-02 blanchet 2011-05-02 tuning
2011-05-02 blanchet 2011-05-02 have each ATP filter out dangerous facts for themselves, based on their type system
2011-05-02 wenzelm 2011-05-02 merged
2011-05-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-05-02 blanchet 2011-05-02 make "debug" more verbose and "verbose" less verbose
2011-05-02 blanchet 2011-05-02 use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
2011-05-02 blanchet 2011-05-02 fixed random number invocation
2011-05-01 blanchet 2011-05-01 use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...
2011-05-01 blanchet 2011-05-01 restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
2011-05-01 blanchet 2011-05-01 take "partial_types" option with a grain of salt
2011-05-01 blanchet 2011-05-01 fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
2011-05-01 blanchet 2011-05-01 implement the new ATP type system in Sledgehammer
2011-05-01 blanchet 2011-05-01 define type system in ATP module so that ATPs can suggest a type system
2011-05-01 blanchet 2011-05-01 made the format (TFF or FOF) of the TPTP problem a global argument of the problem again and have the ATPs report which formats they support
2011-05-01 blanchet 2011-05-01 no needless "fequal" proxies if "explicit_apply" is set + always have readable names
2011-05-01 blanchet 2011-05-01 make sure the minimizer monomorphizes when it should
2011-05-01 blanchet 2011-05-01 reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
2011-05-01 blanchet 2011-05-01 perform constant mangling and/or removal of its type args in an earlier phase, so that the rest of the code doesn't need to worry about it
2011-05-01 blanchet 2011-05-01 move type declarations to the front, for TFF-compliance
2011-05-01 blanchet 2011-05-01 added (without implementation yet) new type encodings for Sledgehammer/ATP
2011-05-01 blanchet 2011-05-01 get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
2011-04-22 blanchet 2011-04-22 iterate the unsound-fact-set removal process to recover even more unsound proofs
2011-04-22 blanchet 2011-04-22 automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
2011-04-21 blanchet 2011-04-21 automatically retry with full-types upon unsound proof
2011-04-21 blanchet 2011-04-21 detect some unsound proofs before showing them to the user
2011-04-21 blanchet 2011-04-21 tuning -- local semicolon consistency
2011-04-21 blanchet 2011-04-21 tuning
2011-04-21 blanchet 2011-04-21 fixed interaction between monomorphization and slicing for ATPs
2011-04-21 blanchet 2011-04-21 cleanup: get rid of "may_slice" arguments without changing semantics
2011-04-21 blanchet 2011-04-21 implemented general slicing for ATPs, especially E 1.2w and above
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-01 blanchet 2011-04-01 remove workaround 8f25605e646c, which is no longer necessary thanks to 173b0f488428
2011-04-01 boehmes 2011-04-01 make configuration of (SMT) full monomorphization more flexible: turn boolean argument into a configuration option
2011-03-31 boehmes 2011-03-31 provide a flag controlling whether all provided facts should be instantiated, possibly inventing new types (which does not work well with Sledgehammer)
2011-03-31 blanchet 2011-03-31 start monomorphization process with subgoal, not entire goal, to avoid needless instances (and only print monomorphization messages in debug mode)
2011-03-31 blanchet 2011-03-31 temporary workaround: filter out spurious monomorphic instances
2011-03-31 blanchet 2011-03-31 added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
2011-03-24 blanchet 2011-03-24 more precise failure reporting in Sledgehammer/SMT
2011-03-22 blanchet 2011-03-22 let SMT errors through -- the main reason for keeping them quiet was that the SMT bridge used to suffer from internal bugs, but these have been fixed for some time now
2011-03-22 blanchet 2011-03-22 make Minimizer honor "verbose" and "debug" options better
2011-03-17 blanchet 2011-03-17 add option to function to keep trivial ATP formulas, needed for some experiments
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-02-21 blanchet 2011-02-21 exit code 127 can mean many things -- not just (and probably not) Perl missing
2011-02-21 blanchet 2011-02-21 give more weight to Frees than to Consts in relevance filter