| Tue, 24 May 2011 10:01:03 +0200 |
blanchet |
more work on parsing LEO-II proofs and extracting uses of extensionality
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
slightly gracefuller handling of LEO-II and Satallax output
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
identify HOL functions with THF functions
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
started adding support for THF output (but no lambdas)
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
tuning -- the "appropriate" terminology is inspired from TPTP
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
improved Waldmeister support -- even run it by default on unit equational goals
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:51:41 +0200 |
blanchet |
fish out axioms in Waldmeister output
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:51:01 +0200 |
blanchet |
added support for remote Waldmeister
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:49:35 +0200 |
blanchet |
reorganized ATP formats a little bit
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
make sure the Vampire incomplete proof detection code kicks in
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
automatically use "metisFT" when typed helpers are necessary
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
more informative message when Sledgehammer finds an unsound proof
|
file |
diff |
annotate
|
| Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
tweaked ATP type systems further based on Judgment Day
|
file |
diff |
annotate
|
| Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)
|
file |
diff |
annotate
|
| Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
renamed thin to light, fat to heavy
|
file |
diff |
annotate
|
| Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
run blacklist algorithm only if slicing is on
|
file |
diff |
annotate
|
| Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
renamed "shallow" to "thin" and make it the default
|
file |
diff |
annotate
|
| Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
added syntax for "shallow" encodings
|
file |
diff |
annotate
|
| Fri, 13 May 2011 10:10:43 +0200 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
| Fri, 13 May 2011 10:10:43 +0200 |
blanchet |
fixed off-by-one bug
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
robustly detect how many type args were passed to the ATP, even if some of them were omitted
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
remove unused parameter
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
reduced penalty associated with existential quantifiers
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
tune whitespace
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
allow each slice to have its own type system
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
renamed type systems for more consistency
|
file |
diff |
annotate
|
| Fri, 06 May 2011 13:34:59 +0200 |
blanchet |
allow each prover to specify its own formula kind for symbols occurring in the conjecture
|
file |
diff |
annotate
|
| Thu, 05 May 2011 12:40:48 +0200 |
blanchet |
no lies in debug output (e.g. "slice 2 of 1")
|
file |
diff |
annotate
|
| Wed, 04 May 2011 22:56:33 +0200 |
blanchet |
renamed "many_typed" to "simple" (as in simple types)
|
file |
diff |
annotate
|
| Wed, 04 May 2011 22:47:13 +0200 |
blanchet |
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
|
file |
diff |
annotate
|
| Tue, 03 May 2011 21:46:49 +0200 |
blanchet |
fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
|
file |
diff |
annotate
|
| Tue, 03 May 2011 01:04:03 +0200 |
blanchet |
no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
|
file |
diff |
annotate
|
| Tue, 03 May 2011 00:10:22 +0200 |
blanchet |
replaced some Unsynchronized.refs with Config.Ts
|
file |
diff |
annotate
|
| Mon, 02 May 2011 22:52:15 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 02 May 2011 22:52:15 +0200 |
blanchet |
have each ATP filter out dangerous facts for themselves, based on their type system
|
file |
diff |
annotate
|
| Mon, 02 May 2011 17:43:42 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Mon, 02 May 2011 15:01:36 +0200 |
blanchet |
make "debug" more verbose and "verbose" less verbose
|
file |
diff |
annotate
|
| Mon, 02 May 2011 14:40:57 +0200 |
blanchet |
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
|
file |
diff |
annotate
|
| Mon, 02 May 2011 14:10:09 +0200 |
blanchet |
fixed random number invocation
|
file |
diff |
annotate
|
| Sun, 01 May 2011 22:36:58 +0200 |
blanchet |
use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
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"
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
take "partial_types" option with a grain of salt
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
implement the new ATP type system in Sledgehammer
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
define type system in ATP module so that ATPs can suggest a type system
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
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
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
make sure the minimizer monomorphizes when it should
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
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
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
move type declarations to the front, for TFF-compliance
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added (without implementation yet) new type encodings for Sledgehammer/ATP
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:23 +0200 |
blanchet |
get rid of "explicit_forall" prover-specific option, even if that means some clutter -- foralls will be necessary to attach types to variables
|
file |
diff |
annotate
|