| Wed, 07 Sep 2011 09:10:41 +0200 |
rationalize uniform encodings
|
file | diff | annotate |
| Tue, 06 Sep 2011 18:13:36 +0200 |
added dummy polymorphic THF system
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:46 +0200 |
cleaner "pff" dummy TFF0 prover
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:45 +0200 |
extended simple types with polymorphism -- the implementation still needs some work though
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:45 +0200 |
added dummy PFF prover, for debugging purposes
|
file | diff | annotate |
| Tue, 30 Aug 2011 16:07:34 +0200 |
first step towards polymorphic TFF + changed defaults for Vampire
|
file | diff | annotate |
| Tue, 30 Aug 2011 14:12:55 +0200 |
improved handling of induction rules in Sledgehammer
|
file | diff | annotate |
| Tue, 30 Aug 2011 14:12:55 +0200 |
added generation of induction rules
|
file | diff | annotate |
| Fri, 26 Aug 2011 01:18:48 +0200 |
disable TFF for Vampire 1.8 until they've fixed the soundness issues and it's back on SystemOnTPTP
|
file | diff | annotate |
| Thu, 25 Aug 2011 23:55:21 +0200 |
make sure that if slicing is disabled, a non-SOS slice is chosen
|
file | diff | annotate |
| Thu, 25 Aug 2011 22:05:18 +0200 |
make TFF output less explicit where possible
|
file | diff | annotate |
| Thu, 25 Aug 2011 19:09:39 +0200 |
use more appropriate encoding for Z3 TPTP, as confirmed by evaluation
|
file | diff | annotate |
| Thu, 25 Aug 2011 19:05:40 +0200 |
added one more known Z3 failure
|
file | diff | annotate |
| Thu, 25 Aug 2011 14:25:07 +0200 |
rationalized option names -- mono becomes raw_mono and mangled becomes mono
|
file | diff | annotate |
| Wed, 24 Aug 2011 22:12:30 +0200 |
remove Vampire imconplete proof detection -- the bug it was trying to work around has been fixed in version 1.8, and the check is too sensitive anyway
|
file | diff | annotate |
| Tue, 23 Aug 2011 23:18:13 +0200 |
fixed "hBOOL" of existential variables, and generate more helpers
|
file | diff | annotate |
| Tue, 23 Aug 2011 16:37:23 +0200 |
always use TFF if possible
|
file | diff | annotate |
| Tue, 23 Aug 2011 16:07:01 +0200 |
exploit TFF format in Z3 used as ATP, and renamed it "z3_tptp"
|
file | diff | annotate |
| Tue, 23 Aug 2011 15:50:27 +0200 |
updated known failures for Z3 3.0 TPTP
|
file | diff | annotate |
| Tue, 23 Aug 2011 15:15:43 +0200 |
avoid TFF format with older Vampire versions
|
file | diff | annotate |
| Tue, 23 Aug 2011 14:44:19 +0200 |
fixed TFF slicing
|
file | diff | annotate |
| Tue, 23 Aug 2011 14:44:19 +0200 |
kindly ask Vampire to output axiom names
|
file | diff | annotate |
| Tue, 23 Aug 2011 14:44:19 +0200 |
added formats to the slice and use TFF for remote Vampire
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
gracefully handle empty SPASS problems
|
file | diff | annotate |
| Wed, 17 Aug 2011 10:03:58 +0200 |
distinguish THF syntax with and without choice (Satallax vs. LEO-II)
|
file | diff | annotate |
| Tue, 09 Aug 2011 17:33:17 +0200 |
support local HOATPs
|
file | diff | annotate |
| Tue, 09 Aug 2011 17:33:17 +0200 |
LEO-II also supports FOF
|
file | diff | annotate |
| Tue, 09 Aug 2011 09:33:50 +0200 |
renamed E wrappers for consistency with CASC conventions
|
file | diff | annotate |
| Tue, 26 Jul 2011 22:53:06 +0200 |
renamed "preds" encodings to "guards"
|
file | diff | annotate |
| Tue, 26 Jul 2011 14:53:00 +0200 |
give E at least two seconds -- anything else risks causing too early timeouts in the minimizer, because of too conservative time computations in E and eproof scripts
|
file | diff | annotate |
| Sat, 16 Jul 2011 20:52:41 +0200 |
moved bash operations to Isabelle_System (cf. Scala version);
|
file | diff | annotate |
| Wed, 06 Jul 2011 17:19:34 +0100 |
better setup for experimental "z3_atp"
|
file | diff | annotate |
| Fri, 01 Jul 2011 15:53:38 +0200 |
renamed "type_sys" to "type_enc", which is more accurate
|
file | diff | annotate |
| Fri, 01 Jul 2011 15:53:37 +0200 |
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 |
tuning
|
file | diff | annotate |
| Mon, 27 Jun 2011 14:56:32 +0200 |
tweaked comment
|
file | diff | annotate |
| Mon, 27 Jun 2011 13:52:47 +0200 |
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 |
remove experimental trimming feature -- it slowed down things on Linux for some reason
|
file | diff | annotate |
| Mon, 27 Jun 2011 13:52:47 +0200 |
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 |
fiddle with remote ATP settings, based on Judgment Day
|
file | diff | annotate |
| Tue, 21 Jun 2011 17:17:39 +0200 |
provide appropriate type system and number of fact defaults for remote ATPs
|
file | diff | annotate |
| Tue, 21 Jun 2011 17:17:39 +0200 |
tweaked E, SPASS, Vampire setup based on latest Judgment Day results
|
file | diff | annotate |
| Mon, 20 Jun 2011 10:41:02 +0200 |
slightly better setup for E
|
file | diff | annotate |
| Mon, 20 Jun 2011 10:41:02 +0200 |
slightly better setup for SPASS and Vampire as more results have come in
|
file | diff | annotate |
| Mon, 20 Jun 2011 10:41:02 +0200 |
optimized SPASS and Vampire time slices, like E before
|
file | diff | annotate |
| Mon, 20 Jun 2011 10:41:02 +0200 |
optimized E's time slicing, based on latest exhaustive Judgment Day results
|
file | diff | annotate |
| Mon, 20 Jun 2011 10:41:02 +0200 |
deal with ATP time slices in a more flexible/robust fashion
|
file | diff | annotate |
| Sun, 19 Jun 2011 18:12:49 +0200 |
recognize one more E failure message
|
file | diff | annotate |
| Sun, 19 Jun 2011 18:12:49 +0200 |
tweaked TPTP formula kind for typing information used in the conjecture
|
file | diff | annotate |
| Fri, 10 Jun 2011 12:01:15 +0200 |
pass --trim option to "eproof" script to speed up proof reconstruction
|
file | diff | annotate |
| Wed, 08 Jun 2011 16:20:18 +0200 |
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 |
slighly more reasonable Vampire slices (until new monomorphizer is used)
|
file | diff | annotate |
| Mon, 30 May 2011 17:00:38 +0200 |
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 |
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 |
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 |
recognize more ATP failures
|
file | diff | annotate |
| Tue, 24 May 2011 18:04:23 +0200 |
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 |
further reduce the number of facts passed to less used remote ATPs
|
file | diff | annotate |
| Tue, 24 May 2011 10:03:15 +0200 |
pass fewer relevant facts to less used remote systems
|
file | diff | annotate |
| Tue, 24 May 2011 00:01:33 +0200 |
slightly gracefuller handling of LEO-II and Satallax output
|
file | diff | annotate |