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
|
Mon, 22 Dec 2014 14:33:53 +0100 |
wenzelm |
separate module Random;
|
file |
diff |
annotate
|
Fri, 31 Oct 2014 11:36:41 +0100 |
wenzelm |
discontinued obsolete Output.urgent_message;
|
file |
diff |
annotate
|
Tue, 09 Sep 2014 15:33:01 +0200 |
steckerm |
Fixed bug which broke isar proof construction for all ATPs except Waldmeister_new
|
file |
diff |
annotate
|
Tue, 02 Sep 2014 16:38:26 +0200 |
steckerm |
Some work on the new waldmeister integration
|
file |
diff |
annotate
|
Thu, 28 Aug 2014 16:58:27 +0200 |
blanchet |
merged minimize and auto_minimize
|
file |
diff |
annotate
|
Tue, 05 Aug 2014 09:20:00 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 13:06:24 +0200 |
blanchet |
default on 'metis' for ATPs if preplaying is disabled
|
file |
diff |
annotate
|
Mon, 04 Aug 2014 12:28:42 +0200 |
blanchet |
rationalized sorting of facts -- so that preplaying (almost always) coincides with the real thing, preventing odd failures
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
restored a bit of laziness
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
honor 'try0' also for one-liners
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated needlessly complex message tail
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
eliminated Sledgehammer's "min" subcommand (and lots of complications in the code)
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
rationalized preplaying by eliminating (now superfluous) laziness
|
file |
diff |
annotate
|
Fri, 01 Aug 2014 14:43:57 +0200 |
blanchet |
simplified minimization logic
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
use parallel preplay machinery also for one-line proofs
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 23:52:56 +0200 |
blanchet |
always minimize Sledgehammer results by default
|
file |
diff |
annotate
|
Wed, 30 Jul 2014 14:03:12 +0200 |
fleury |
imported patch satallax_proof_support_Sledgehammer
|
file |
diff |
annotate
|
Fri, 25 Jul 2014 11:26:17 +0200 |
blanchet |
avoid 'eproof' and 'eproof_ram' scripts if possible (i.e. if 'eprover' can produce reasonable enough proofs for one-liner reconstruction)
|
file |
diff |
annotate
|
Tue, 01 Jul 2014 16:47:10 +0200 |
blanchet |
speed up MaSh a bit
|
file |
diff |
annotate
|
Mon, 16 Jun 2014 19:42:44 +0200 |
blanchet |
integrated new Waldmeister code with 'sledgehammer' command
|
file |
diff |
annotate
|
Mon, 16 Jun 2014 19:41:42 +0200 |
blanchet |
fixed parsing of one-argument 'file()' in TSTP files
|
file |
diff |
annotate
|
Mon, 16 Jun 2014 19:40:59 +0200 |
blanchet |
simplified code
|
file |
diff |
annotate
|
Mon, 16 Jun 2014 16:21:52 +0200 |
fleury |
Moving the remote prefix deleting on Sledgehammer's side
|
file |
diff |
annotate
|
Mon, 16 Jun 2014 16:18:15 +0200 |
fleury |
add support for Isar reconstruction for thf1 ATP provers like Leo-II.
|
file |
diff |
annotate
|
Thu, 12 Jun 2014 17:10:12 +0200 |
blanchet |
renamed Sledgehammer options
|
file |
diff |
annotate
|
Mon, 02 Jun 2014 15:10:18 +0200 |
fleury |
basic setup for zipperposition prover
|
file |
diff |
annotate
|
Thu, 22 May 2014 03:29:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
Thu, 13 Feb 2014 13:16:17 +0100 |
blanchet |
avoid changing the state's context -- this results in transfer problems later with SMT, and hence preplay tactic failures
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 23:38:33 +0100 |
blanchet |
properly overwrite replay data from one compression iteration to another
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 23:20:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 19:32:02 +0100 |
blanchet |
tuned behavior of 'smt' option
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 17:13:31 +0100 |
blanchet |
added 'smt' option to control generation of 'by smt' proofs
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 16:53:58 +0100 |
blanchet |
renamed ML file
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 15:19:07 +0100 |
blanchet |
merged 'reconstructors' and 'proof methods'
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
Mon, 03 Feb 2014 10:14:18 +0100 |
blanchet |
got rid of 'try0' step that is now redundant
|
file |
diff |
annotate
|
Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
rationalized threading of 'metis' arguments
|
file |
diff |
annotate
|
Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Sun, 02 Feb 2014 20:53:51 +0100 |
blanchet |
made SML/NJ happier
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 16:10:39 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 13:42:47 +0100 |
blanchet |
compile
|
file |
diff |
annotate
|
Fri, 31 Jan 2014 12:30:54 +0100 |
blanchet |
refactor large ML file
|
file |
diff |
annotate
|