Tue, 29 Jun 2010 09:26:56 +0200 |
blanchet |
rename "skolem_somes" to "skolems", now that there's only one flavor of Skolems
|
file |
diff |
annotate
|
Tue, 29 Jun 2010 09:05:37 +0200 |
blanchet |
move functions not needed by Metis out of "Metis_Clauses"
|
file |
diff |
annotate
|
Mon, 28 Jun 2010 18:46:42 +0200 |
blanchet |
adapt call
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 17:26:14 +0200 |
blanchet |
got rid of "respect_no_atp" option, which even I don't use
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 17:08:39 +0200 |
blanchet |
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 16:42:06 +0200 |
blanchet |
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 16:15:03 +0200 |
blanchet |
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
|
file |
diff |
annotate
|
Fri, 25 Jun 2010 12:07:52 +0200 |
blanchet |
split SPASS time slot between SOS and non-SOS, in case SOS times out
|
file |
diff |
annotate
|
Wed, 23 Jun 2010 11:36:03 +0200 |
blanchet |
if SPASS fails at finding a proof with the SOS option turned on, turn it off and try again
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 23:54:02 +0200 |
blanchet |
factor out TPTP format output into file of its own, to facilitate further changes
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 18:47:45 +0200 |
blanchet |
missing "Unsynchronized" + make exception take a unit
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 14:48:46 +0200 |
blanchet |
merge "generic_prover" and "generic_tptp_prover"
|
file |
diff |
annotate
|
Tue, 22 Jun 2010 14:28:22 +0200 |
blanchet |
removed Sledgehammer's support for the DFG syntax;
|
file |
diff |
annotate
|
Mon, 21 Jun 2010 12:33:43 +0200 |
blanchet |
thread "full_types"
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 17:12:41 +0200 |
blanchet |
better error reporting for Vampire
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 16:43:44 +0200 |
blanchet |
expect SPASS 3.7, and give a friendly warning if an older version is used
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 16:17:20 +0200 |
blanchet |
improve ATP-specific error messages
|
file |
diff |
annotate
|
Sat, 05 Jun 2010 16:39:23 +0200 |
blanchet |
show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
|
file |
diff |
annotate
|
Sat, 05 Jun 2010 16:08:35 +0200 |
blanchet |
fix remote Vampire diagnosis
|
file |
diff |
annotate
|
Fri, 04 Jun 2010 16:54:10 +0200 |
blanchet |
recongize one more outcome string for "remote_vampire"
|
file |
diff |
annotate
|
Fri, 28 May 2010 13:49:21 +0200 |
blanchet |
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
|
file |
diff |
annotate
|
Mon, 17 May 2010 10:16:54 +0200 |
blanchet |
identify common SPASS error more clearly
|
file |
diff |
annotate
|
Fri, 14 May 2010 22:29:50 +0200 |
blanchet |
renamed options
|
file |
diff |
annotate
|
Fri, 14 May 2010 16:15:10 +0200 |
blanchet |
renamed two Sledgehammer options
|
file |
diff |
annotate
|
Fri, 14 May 2010 15:26:26 +0200 |
blanchet |
query _HOME environment variables at run-time, not at build-time
|
file |
diff |
annotate
|
Fri, 14 May 2010 11:24:14 +0200 |
blanchet |
pass "full_type" argument to proof reconstruction
|
file |
diff |
annotate
|
Thu, 29 Apr 2010 19:08:02 +0200 |
blanchet |
in "overlord" mode: ignore problem prefix specified in the .thy file
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 22:00:48 +0200 |
blanchet |
back to Vampire 9 -- Vampire 11 sometimes outputs really weird proofs
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 17:56:07 +0200 |
blanchet |
properly extract SPASS proof
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 17:47:30 +0200 |
blanchet |
try out Vampire 11 and parse its output correctly;
|
file |
diff |
annotate
|
Wed, 28 Apr 2010 13:32:45 +0200 |
blanchet |
removed "sorts" option, continued
|
file |
diff |
annotate
|
Tue, 27 Apr 2010 18:58:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 27 Apr 2010 11:24:47 +0200 |
blanchet |
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
|
file |
diff |
annotate
|
Mon, 26 Apr 2010 21:17:41 +0200 |
blanchet |
rename options and keep track of conjecture shape (to facilitate proof reconstruction)
|
file |
diff |
annotate
|
Sun, 25 Apr 2010 11:38:46 +0200 |
blanchet |
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
|
file |
diff |
annotate
|
Fri, 23 Apr 2010 19:36:49 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
Fri, 23 Apr 2010 18:11:41 +0200 |
blanchet |
now rename the file "atp_wrapper.ML" to "atp_systems.ML" + fix typo in "SystemOnTPTP" script
|
file |
diff |
annotate
| base
|