| Fri, 20 Jul 2012 22:19:45 +0200 |
renamed ML structures
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:04 +0200 |
learn from minimized ATP proofs
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
centrally construct expensive data structures
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
renamed Sledgehammer options
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
more code rationalization in relevance filter
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
systematize lazy names in relevance filter
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
rationalize relevance filter, slowing moving code from Iter to MaSh
|
file | diff | annotate |
| Wed, 11 Jul 2012 21:43:19 +0200 |
further ML structure split to permit finer-grained loading/reordering (problem to solve: MaSh needs most of Sledgehammer)
|
file | diff | annotate |
| Wed, 23 May 2012 21:19:48 +0200 |
improved LEO-II definition handling -- still hoping for a fix directly in LEO-II
|
file | diff | annotate |
| Wed, 23 May 2012 21:19:48 +0200 |
better handling of incomplete TSTP proofs
|
file | diff | annotate |
| Wed, 02 May 2012 11:47:45 +0200 |
updated headers;
|
file | diff | annotate |
| Tue, 24 Apr 2012 14:13:04 +0100 |
merged
|
file | diff | annotate | base |
| Tue, 24 Apr 2012 13:59:29 +0100 |
reversed Tools to Actions Mirabelle renaming;
|
file | diff | annotate | base |
| Fri, 30 Mar 2012 00:01:30 +0100 |
made Mirabelle-SH's 'trivial' check optional;
|
file | diff | annotate |
| Tue, 27 Mar 2012 16:59:13 +0300 |
more robustness in case a theorem cannot be retrieved (which typically happens with backtick facts)
|
file | diff | annotate |
| Wed, 21 Mar 2012 11:00:34 +0100 |
prefer explicitly qualified exception List.Empty;
|
file | diff | annotate |
| Tue, 20 Mar 2012 13:53:09 +0100 |
added term_order option to Mirabelle
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
more weight attribute tuning
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
internal renamings
|
file | diff | annotate |
| Wed, 07 Mar 2012 13:00:30 +0000 |
added max_new_mono_instances, max_mono_iters, to Mirabelle-Sledgehammer; changed sh_minimize to avoid setting Mirabelle-level defaults;
|
file | diff | annotate |
| Wed, 07 Mar 2012 13:00:30 +0000 |
added sh_minimize and preplay_timeout options to Mirabelle's Sledgehammer action;
|
file | diff | annotate |
| Fri, 24 Feb 2012 11:23:34 +0100 |
renamed 'try_methods' to 'try0'
|
file | diff | annotate |
| Mon, 06 Feb 2012 23:01:01 +0100 |
renamed type encoding
|
file | diff | annotate |
| Sun, 05 Feb 2012 12:27:10 +0100 |
tuning
|
file | diff | annotate |
| Sat, 04 Feb 2012 17:01:25 +0100 |
added option to Mirabelle/Sledgehammer
|
file | diff | annotate |
| Tue, 31 Jan 2012 18:46:31 +0100 |
renamed Sledgehammer option
|
file | diff | annotate |
| Mon, 30 Jan 2012 17:15:59 +0100 |
rename lambda translation schemes
|
file | diff | annotate |
| Thu, 26 Jan 2012 20:49:54 +0100 |
separate orthogonal components
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:32 +0100 |
renamed two files to make room for a new file
|
file | diff | annotate |
| Thu, 01 Dec 2011 13:34:13 +0100 |
renamed "slicing" to "slice"
|
file | diff | annotate |
| Wed, 16 Nov 2011 16:35:19 +0100 |
thread in additional options to minimizer
|
file | diff | annotate |
| Wed, 16 Nov 2011 13:22:36 +0100 |
make metis reconstruction handling more flexible
|
file | diff | annotate |
| Wed, 16 Nov 2011 09:42:27 +0100 |
parse lambda translation option in Metis
|
file | diff | annotate |
| Tue, 15 Nov 2011 22:15:51 +0100 |
rename configuration option to more reasonable length
|
file | diff | annotate |
| Sun, 06 Nov 2011 14:05:57 +0100 |
tuning
|
file | diff | annotate |
| Wed, 07 Sep 2011 09:10:41 +0200 |
rationalize uniform encodings
|
file | diff | annotate |
| Fri, 02 Sep 2011 14:43:20 +0200 |
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
|
file | diff | annotate |
| Thu, 01 Sep 2011 13:18:27 +0200 |
always measure time for ATPs -- auto minimization relies on it
|
file | diff | annotate |
| Thu, 01 Sep 2011 13:18:27 +0200 |
make "sound" sound and "unsound" more sound, based on evaluation
|
file | diff | annotate |
| Wed, 31 Aug 2011 11:52:03 +0200 |
more tuning
|
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 14:12:55 +0200 |
improved handling of induction rules in Sledgehammer
|
file | diff | annotate |
| Sun, 28 Aug 2011 13:13:27 +0200 |
split timeout among ATPs in and add Metis to the mix as backup
|
file | diff | annotate |
| Sat, 27 Aug 2011 11:22:21 +0200 |
beef up sledgehammer_tac in Mirabelle some more
|
file | diff | annotate |
| Thu, 25 Aug 2011 00:00:36 +0200 |
include chained facts for minimizer, otherwise it won't work
|
file | diff | annotate |
| Wed, 24 Aug 2011 11:17:33 +0200 |
more reliable "sledgehammer\_tac" reconstruction, by avoiding "insert_tac"
|
file | diff | annotate |
| Wed, 24 Aug 2011 11:17:33 +0200 |
specify timeout for "sledgehammer_tac"
|
file | diff | annotate |
| Tue, 23 Aug 2011 22:44:08 +0200 |
don't select facts when using sledgehammer_tac for reconstruction
|
file | diff | annotate |
| Tue, 23 Aug 2011 20:35:41 +0200 |
don't perform a triviality check if the goal is skipped anyway
|
file | diff | annotate |
| Tue, 23 Aug 2011 19:50:25 +0200 |
optional reconstructor
|
file | diff | annotate |
| Tue, 23 Aug 2011 19:00:48 +0200 |
added "max_calls" option to get a fixed number of Sledgehammer calls per theory
|
file | diff | annotate |
| Tue, 23 Aug 2011 18:42:05 +0200 |
beef up "sledgehammer_tac" reconstructor
|
file | diff | annotate |
| Tue, 23 Aug 2011 16:14:19 +0200 |
clearer separator in generated file names
|
file | diff | annotate |
| Tue, 09 Aug 2011 17:33:17 +0200 |
support local HOATPs
|
file | diff | annotate |
| Tue, 09 Aug 2011 09:24:34 +0200 |
add line number prefix to output file name
|
file | diff | annotate |
| Tue, 09 Aug 2011 09:07:59 +0200 |
added "sound" option to Mirabelle
|
file | diff | annotate |
| Wed, 20 Jul 2011 00:37:42 +0200 |
remove offset from Mirabelle output
|
file | diff | annotate |
| Thu, 14 Jul 2011 16:50:05 +0200 |
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
|
file | diff | annotate |
| Thu, 14 Jul 2011 16:50:05 +0200 |
added option to control which lambda translation to use (for experiments)
|
file | diff | annotate |
| Fri, 08 Jul 2011 17:04:38 +0200 |
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
|
file | diff | annotate |