Wed, 06 Jul 2011 17:19:34 +0100 |
blanchet |
better setup for experimental "z3_atp"
|
file |
diff |
annotate
|
Fri, 01 Jul 2011 15:53:38 +0200 |
blanchet |
renamed "type_sys" to "type_enc", which is more accurate
|
file |
diff |
annotate
|
Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
cleaner handling of higher-order simple types, so that it's also possible to use first-order simple types with LEO-II and company
|
file |
diff |
annotate
|
Fri, 01 Jul 2011 15:53:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 14:56:32 +0200 |
blanchet |
tweaked comment
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
removed "full_types" option from Sledgehammer, now that virtually sound encodings are used as the default anyway
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
remove experimental trimming feature -- it slowed down things on Linux for some reason
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 13:52:47 +0200 |
blanchet |
filter out some tautologies using an ATP, especially for those theories that are known for producing such things
|
file |
diff |
annotate
|
Thu, 23 Jun 2011 11:19:41 +0200 |
blanchet |
fiddle with remote ATP settings, based on Judgment Day
|
file |
diff |
annotate
|
Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
provide appropriate type system and number of fact defaults for remote ATPs
|
file |
diff |
annotate
|
Tue, 21 Jun 2011 17:17:39 +0200 |
blanchet |
tweaked E, SPASS, Vampire setup based on latest Judgment Day results
|
file |
diff |
annotate
|
Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
slightly better setup for E
|
file |
diff |
annotate
|
Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
slightly better setup for SPASS and Vampire as more results have come in
|
file |
diff |
annotate
|
Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
optimized SPASS and Vampire time slices, like E before
|
file |
diff |
annotate
|
Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
optimized E's time slicing, based on latest exhaustive Judgment Day results
|
file |
diff |
annotate
|
Mon, 20 Jun 2011 10:41:02 +0200 |
blanchet |
deal with ATP time slices in a more flexible/robust fashion
|
file |
diff |
annotate
|
Sun, 19 Jun 2011 18:12:49 +0200 |
blanchet |
recognize one more E failure message
|
file |
diff |
annotate
|
Sun, 19 Jun 2011 18:12:49 +0200 |
blanchet |
tweaked TPTP formula kind for typing information used in the conjecture
|
file |
diff |
annotate
|
Fri, 10 Jun 2011 12:01:15 +0200 |
blanchet |
pass --trim option to "eproof" script to speed up proof reconstruction
|
file |
diff |
annotate
|
Wed, 08 Jun 2011 16:20:18 +0200 |
blanchet |
better default type system for Waldmeister, with fewer predicates (for types or type classes)
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 23:46:02 +0200 |
blanchet |
slighly more reasonable Vampire slices (until new monomorphizer is used)
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
avoid monomorphic encoding with so many facts -- it makes the old monomorphizer explode on some examples
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
no more bonus for E -- with the soft timeout, this punishes everybody -- the bonus was designed for a hard timeout
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
recognize more ATP failures
|
file |
diff |
annotate
|
Tue, 24 May 2011 18:04:23 +0200 |
blanchet |
ensure that the argument of logical negation is enclosed in parentheses in THF mode
|
file |
diff |
annotate
|
Tue, 24 May 2011 13:29:32 +0200 |
blanchet |
further reduce the number of facts passed to less used remote ATPs
|
file |
diff |
annotate
|
Tue, 24 May 2011 10:03:15 +0200 |
blanchet |
pass fewer relevant facts to less used remote systems
|
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 |
clearer SystemOnTPTP errors
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
give fewer equations to Waldmeister
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
detect inappropriate problems and crashes better in Waldmeister
|
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:04 +0200 |
blanchet |
recognize one more SystemOnTPTP error
|
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:50:32 +0200 |
blanchet |
added 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
|
Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
renamed "simple_types" to "simple"
|
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 |
better error reporting: detect missing E proofs and remove Vampire native format error
|
file |
diff |
annotate
|
Fri, 13 May 2011 10:10:43 +0200 |
blanchet |
tweak E slices
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
drop support for Vampire's native output format -- it has too many undocumented oddities, e.g. "BDD definition:" lines
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
added "force_sos" options to control SPASS's and Vampire's use of SOS in experiments + added corresponding Mirabelle options
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
allow each slice to have its own type system
|
file |
diff |
annotate
|
Fri, 06 May 2011 13:35:00 +0200 |
blanchet |
further improved type system setup based on Judgment Days
|
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
|
Fri, 06 May 2011 13:34:59 +0200 |
blanchet |
better type system setup, based on Judgment Day
|
file |
diff |
annotate
|
Thu, 05 May 2011 09:43:39 +0200 |
blanchet |
improve suggested type system list based on evaluation
|
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 08:52:32 +0200 |
blanchet |
whitespace tuning
|
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 |
better default type systems for SNARK and ToFoF
|
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:22:34 +0200 |
blanchet |
supply type-system defaults for major ATPs
|
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
|