| Sat, 19 Dec 2015 20:02:51 +0100 |
blanchet |
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
|
file |
diff |
annotate
|
| Mon, 05 Oct 2015 13:26:25 +0200 |
blanchet |
extended theory exporter to also export MePo-selected facts
|
file |
diff |
annotate
|
| Thu, 13 Aug 2015 11:05:19 +0200 |
wenzelm |
tuned signature, in accordance to sortBy in Scala;
|
file |
diff |
annotate
|
| Fri, 03 Jul 2015 16:19:45 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
SPASS-Pirate is now called Pirate
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 15:42:34 +0100 |
wenzelm |
proper Keyword.keywords (cf. 82a71046dce8);
|
file |
diff |
annotate
|
| Fri, 25 Jul 2014 12:22:18 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 15:49:20 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 24 Jun 2014 15:08:19 +0200 |
blanchet |
optimized traversal of proof terms by skipping bad apples (e.g. full_exhaustive_int'.pinduct)
|
file |
diff |
annotate
|
| 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
|