Mon, 16 Jun 2014 19:44:02 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Tue, 17 Dec 2013 14:03:29 +0100 |
blanchet |
primitive support for SPASS-Pirate (Daniel Wand's polymorphic SPASS prototype)
|
file |
diff |
annotate
|
Thu, 24 Oct 2013 12:43:33 +0200 |
blanchet |
use definitions for LEO-II as well -- this simplifies the code and matches some users' expectations
|
file |
diff |
annotate
|
Sun, 29 Sep 2013 12:21:11 +0200 |
wenzelm |
made SML/NJ happy (NB: toplevel ML environment is unmanaged);
|
file |
diff |
annotate
|
Thu, 12 Sep 2013 22:10:57 +0200 |
blanchet |
prefixed types and some functions with "atp_" for disambiguation
|
file |
diff |
annotate
|
Tue, 13 Aug 2013 10:26:56 +0200 |
blanchet |
Vampire 3.0 requires types to be declared -- make it happy (and get rid of "implicit" types since only Satallax seems to support them anymore)
|
file |
diff |
annotate
|
Mon, 29 Jul 2013 15:30:31 +0200 |
blanchet |
added support for E 1.8's internal proof objects (eliminating the need for "eproof_ram")
|
file |
diff |
annotate
|
Thu, 16 May 2013 13:34:13 +0200 |
blanchet |
tuning -- renamed '_from_' to '_of_' in Sledgehammer
|
file |
diff |
annotate
|
Wed, 15 May 2013 17:43:42 +0200 |
blanchet |
renamed Sledgehammer functions with 'for' in their names to 'of'
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 16:32:04 +0200 |
blanchet |
handle case clashes on Mac file system by encoding goal numbers
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 15:19:14 +0200 |
blanchet |
smoothly handle cyclic graphs
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 15:19:14 +0200 |
blanchet |
compile + fixed naming convention
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 15:19:14 +0200 |
blanchet |
no need to filter tautologies anymore -- they are prefiltered by "all_facts"'
|
file |
diff |
annotate
|
Tue, 09 Apr 2013 15:19:14 +0200 |
blanchet |
work on CASC LTB ISA exporter
|
file |
diff |
annotate
|
Mon, 08 Apr 2013 14:16:00 +0200 |
blanchet |
try to preserve original linearization
|
file |
diff |
annotate
|
Mon, 08 Apr 2013 12:27:13 +0200 |
blanchet |
use somewhat lighter encoding
|
file |
diff |
annotate
|
Thu, 17 Jan 2013 14:01:45 +0100 |
blanchet |
added E-Par support
|
file |
diff |
annotate
|
Fri, 04 Jan 2013 21:56:20 +0100 |
blanchet |
refined class handling, to prevent cycles in fact graph
|
file |
diff |
annotate
|
Thu, 13 Dec 2012 22:49:08 +0100 |
blanchet |
generate comments with original names for debugging
|
file |
diff |
annotate
|
Wed, 12 Dec 2012 02:47:45 +0100 |
blanchet |
merge aliased theorems in MaSh dependencies, modulo symmetry of equality
|
file |
diff |
annotate
|
Sat, 08 Dec 2012 21:54:28 +0100 |
blanchet |
don't blacklist "case" theorems -- this causes problems in MaSh later
|
file |
diff |
annotate
|
Tue, 07 Aug 2012 14:29:18 +0200 |
blanchet |
stop distinguishing between complete and incomplete slices, since this is very fragile and has hardly any useful semantics to users
|
file |
diff |
annotate
|
Thu, 26 Jul 2012 10:48:03 +0200 |
blanchet |
repaired accessibility chains generated by MaSh exporter + tuned one function out
|
file |
diff |
annotate
|
Mon, 23 Jul 2012 15:32:30 +0200 |
blanchet |
distinguish between recursive and nonrecursive definitions + clean up typedef dependencies in MaSh
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
honor suggested MaSh weights
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:46 +0200 |
blanchet |
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 |
blanchet |
renamed ML structures
|
file |
diff |
annotate
|
Fri, 20 Jul 2012 22:19:45 +0200 |
blanchet |
use "eproof_ram" script if available (plug-in replacement for "eproof", but faster)
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
speed up tautology/metaness check
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
more consolidation of MaSh code
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
drastic overhaul of MaSh data structures + fixed a few performance issues
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:04 +0200 |
blanchet |
fixed order of accessibles + other tweaks to MaSh
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
started implementing MaSh client-side I/O
|
file |
diff |
annotate
|
Wed, 18 Jul 2012 08:44:03 +0200 |
blanchet |
centrally construct expensive data structures
|
file |
diff |
annotate
|
Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
moved most of MaSh exporter code to Sledgehammer
|
file |
diff |
annotate
|
Wed, 11 Jul 2012 21:43:19 +0200 |
blanchet |
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 |
blanchet |
MaSh evaluation driver
|
file |
diff |
annotate
|
Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
moved MaSh into own files
|
file |
diff |
annotate
|
Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
distinguish updates and queries + cleanups
|
file |
diff |
annotate
|
Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
better tautology elimination
|
file |
diff |
annotate
|
Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
generate lambdas and skolems again
|
file |
diff |
annotate
|
Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
generate deep terms as feature
|
file |
diff |
annotate
|
Tue, 10 Jul 2012 23:36:03 +0200 |
blanchet |
generate theory name as a feature
|
file |
diff |
annotate
|
Mon, 09 Jul 2012 23:58:05 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Mon, 09 Jul 2012 23:23:12 +0200 |
blanchet |
more precise dependencies -- eliminate tautologies
|
file |
diff |
annotate
|
Mon, 09 Jul 2012 23:23:12 +0200 |
blanchet |
generate problem file
|
file |
diff |
annotate
|
Mon, 09 Jul 2012 23:23:12 +0200 |
blanchet |
improve feature list generation
|
file |
diff |
annotate
|
Mon, 09 Jul 2012 23:23:12 +0200 |
blanchet |
cleaner accessibility file
|
file |
diff |
annotate
|
Mon, 09 Jul 2012 23:23:12 +0200 |
blanchet |
first go at generating files for MaSh (machine-learning Sledgehammer)
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
finished implementation of DFG type class output
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
more work on class support
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:40 +0200 |
blanchet |
cleanly distinguish between type declarations and symbol declarations
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
added type arguments to "ATerm" constructor -- but don't use them yet
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
started adding polymophic SPASS output
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 26 Jun 2012 11:14:39 +0200 |
blanchet |
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 |
blanchet |
start phasing out old SPASS
|
file |
diff |
annotate
|
Mon, 21 May 2012 10:39:32 +0200 |
blanchet |
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 |
blanchet |
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 |
blanchet |
true delayed evaluation of "SPASS_VERSION" environment variable
|
file |
diff |
annotate
|