| Fri, 20 Jul 2012 22:19:46 +0200 |
honor suggested MaSh weights
|
file | diff | annotate |
| Fri, 20 Jul 2012 22:19:46 +0200 |
fixed various issues with MaSh's file handling + tune output + generate local facts again + handle nameless facts gracefully
|
file | diff | annotate |
| Fri, 20 Jul 2012 22:19:45 +0200 |
renamed ML structures
|
file | diff | annotate |
| Fri, 20 Jul 2012 22:19:45 +0200 |
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:04 +0200 |
speed up tautology/metaness check
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:04 +0200 |
more consolidation of MaSh code
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:04 +0200 |
drastic overhaul of MaSh data structures + fixed a few performance issues
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:04 +0200 |
fixed order of accessibles + other tweaks to MaSh
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
started implementing MaSh client-side I/O
|
file | diff | annotate |
| Wed, 18 Jul 2012 08:44:03 +0200 |
centrally construct expensive data structures
|
file | diff | annotate |
| Wed, 11 Jul 2012 21:43:19 +0200 |
moved most of MaSh exporter code to Sledgehammer
|
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 |
| Tue, 10 Jul 2012 23:36:03 +0200 |
MaSh evaluation driver
|
file | diff | annotate |
| Tue, 10 Jul 2012 23:36:03 +0200 |
moved MaSh into own files
|
file | diff | annotate |
| Tue, 10 Jul 2012 23:36:03 +0200 |
distinguish updates and queries + cleanups
|
file | diff | annotate |
| Tue, 10 Jul 2012 23:36:03 +0200 |
better tautology elimination
|
file | diff | annotate |
| Tue, 10 Jul 2012 23:36:03 +0200 |
generate lambdas and skolems again
|
file | diff | annotate |
| Tue, 10 Jul 2012 23:36:03 +0200 |
generate deep terms as feature
|
file | diff | annotate |
| Tue, 10 Jul 2012 23:36:03 +0200 |
generate theory name as a feature
|
file | diff | annotate |
| Mon, 09 Jul 2012 23:58:05 +0200 |
compile
|
file | diff | annotate |
| Mon, 09 Jul 2012 23:23:12 +0200 |
more precise dependencies -- eliminate tautologies
|
file | diff | annotate |
| Mon, 09 Jul 2012 23:23:12 +0200 |
generate problem file
|
file | diff | annotate |
| Mon, 09 Jul 2012 23:23:12 +0200 |
improve feature list generation
|
file | diff | annotate |
| Mon, 09 Jul 2012 23:23:12 +0200 |
cleaner accessibility file
|
file | diff | annotate |
| Mon, 09 Jul 2012 23:23:12 +0200 |
first go at generating files for MaSh (machine-learning Sledgehammer)
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:40 +0200 |
finished implementation of DFG type class output
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:40 +0200 |
more work on class support
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:40 +0200 |
cleanly distinguish between type declarations and symbol declarations
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:39 +0200 |
added type arguments to "ATerm" constructor -- but don't use them yet
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:39 +0200 |
started adding polymophic SPASS output
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:39 +0200 |
tuning
|
file | diff | annotate |
| Tue, 26 Jun 2012 11:14:39 +0200 |
removed support for unsorted DFG, now that SPASS 3.7 is no longer supported
|
file | diff | annotate |
| Mon, 21 May 2012 11:31:52 +0200 |
start phasing out old SPASS
|
file | diff | annotate |
| Mon, 21 May 2012 10:39:32 +0200 |
add an experimental "aggressive" mode to Sledgehammer, to experiment with more complete translations of higher-order features without breaking "metis"
|
file | diff | annotate |
| Sun, 13 May 2012 16:31:01 +0200 |
get rid of "conj_sym_kind" -- most interesting provers now have built-in sorts, and for the others (e.g. E) "Hypothesis" isn't too bad a default
|
file | diff | annotate |
| Thu, 19 Apr 2012 17:49:08 +0200 |
true delayed evaluation of "SPASS_VERSION" environment variable
|
file | diff | annotate |
| Tue, 20 Mar 2012 18:42:45 +0100 |
made "spass" a "metaprover" that uses either the new SPASS or the old SPASS, to preserve backward compatibility and prepare for the upcoming release
|
file | diff | annotate |
| Tue, 20 Mar 2012 00:44:30 +0100 |
continued implementation of term ordering attributes
|
file | diff | annotate |
| Tue, 28 Feb 2012 15:54:51 +0100 |
speed up Sledgehammer's clasimpset lookup a bit
|
file | diff | annotate |
| Sat, 25 Feb 2012 13:13:14 +0100 |
standard Graph instances;
|
file | diff | annotate |
| Thu, 09 Feb 2012 12:57:59 +0100 |
added possibility of generating KBO weights to DFG problems
|
file | diff | annotate |
| Sat, 04 Feb 2012 12:08:18 +0100 |
made option available to users (mostly for experiments)
|
file | diff | annotate |
| Fri, 03 Feb 2012 18:00:55 +0100 |
extended SPASS/DFG output with ranks
|
file | diff | annotate |
| Mon, 30 Jan 2012 17:15:59 +0100 |
rename lambda translation schemes
|
file | diff | annotate |
| Mon, 23 Jan 2012 17:40:32 +0100 |
renamed theory exporter
|
file | diff | annotate | base |