| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:21:11 +0200 |
blanchet |
make sure chained facts don't pop up in the metis proof
|
file |
diff |
annotate
|
| Mon, 17 May 2010 12:15:37 +0200 |
blanchet |
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
|
file |
diff |
annotate
|
| Fri, 14 May 2010 22:29:50 +0200 |
blanchet |
renamed options
|
file |
diff |
annotate
|
| Fri, 14 May 2010 11:23:42 +0200 |
blanchet |
made Sledgehammer's full-typed proof reconstruction work for the first time;
|
file |
diff |
annotate
|
| Sat, 01 May 2010 21:29:03 +0200 |
krauss |
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
|
file |
diff |
annotate
|
| Sat, 01 May 2010 20:49:39 +0200 |
krauss |
Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
|
file |
diff |
annotate
|
| Sat, 01 May 2010 10:37:31 +0200 |
blanchet |
now if this doesn't make SML/NJ happy, nothing will
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 14:52:49 +0200 |
blanchet |
eliminate trivial case splits from Isar proofs
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 13:58:35 +0200 |
blanchet |
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 19:07:36 +0200 |
blanchet |
uncomment code
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:45:39 +0200 |
blanchet |
be more discriminate: some one-line Isar proofs are silly
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:39:46 +0200 |
blanchet |
one-step Isar proofs are not always pointless
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:31:08 +0200 |
blanchet |
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 12:21:20 +0200 |
blanchet |
fixed definition of "bad frees" so that it actually works
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 11:38:23 +0200 |
blanchet |
don't remove last line of proof
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 11:22:24 +0200 |
blanchet |
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 10:55:59 +0200 |
blanchet |
make SML/NJ happy, take 2
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 10:25:26 +0200 |
blanchet |
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 01:17:14 +0200 |
blanchet |
expand combinators in Isar proofs constructed by Sledgehammer;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 21:59:29 +0200 |
blanchet |
improve unskolemization
|
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 15:53:17 +0200 |
blanchet |
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 15:34:55 +0200 |
blanchet |
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:00:30 +0200 |
blanchet |
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:46:50 +0200 |
blanchet |
support Vampire definitions of constants as "let" constructs in Isar proofs
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 18:58:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 17:05:39 +0200 |
blanchet |
polish Isar proofs: don't mention facts twice, and don't show one-liner "structured" proofs
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 16:12:51 +0200 |
blanchet |
reintroduce missing "gen_all_vars" call
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 16:00:20 +0200 |
blanchet |
fix types of "fix" variables to help proof reconstruction and aid readability
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 14:55:10 +0200 |
blanchet |
allow schematic variables in types in terms that are reconstructed by Sledgehammer
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 12:07:07 +0200 |
blanchet |
new Isar proof construction code: stringfy axiom names correctly
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 11:44:01 +0200 |
blanchet |
honor "shrink_proof" Sledgehammer option
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 10:51:39 +0200 |
blanchet |
fix SML/NJ compilation (I hope)
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:41:54 +0200 |
blanchet |
make compile (and not just load dynamically)
|
file |
diff |
annotate
|
| Mon, 26 Apr 2010 21:20:43 +0200 |
blanchet |
introduced direct proof reconstruction code, eliminating the need for the "neg_clausify" method;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:30:33 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:04:20 +0200 |
blanchet |
cosmetics
|
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
|
| Sun, 25 Apr 2010 10:22:31 +0200 |
blanchet |
cosmetics: rename internal functions
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 13:16:50 +0200 |
blanchet |
handle ATP proof delimiters in a cleaner, more extensible fashion
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 12:07:12 +0200 |
blanchet |
handle SPASS's equality predicate correctly in Isar proof reconstruction
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 11:32:36 +0200 |
blanchet |
added Isar proof reconstruction support for SPASS -- which means all provers can now yield Isar proofs;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 15:01:36 +0200 |
blanchet |
minor code cleanup
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 14:47:52 +0200 |
blanchet |
if Isar proof reconstruction is not supported, tell the user so they don't wonder why their "isar_proof" option did nothing
|
file |
diff |
annotate
|
| Thu, 22 Apr 2010 10:54:56 +0200 |
blanchet |
Isar proof reconstruction: type variables introduced by the ATP should be treated as type parameters for type inference purposes;
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 17:06:26 +0200 |
blanchet |
failure of reconstructing the Isar proof (e.g., exception) should not prevent Sledgehammer from showing the short one-liner proof -- but in "debug" mode we do want to know what the exception is
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 16:21:19 +0200 |
blanchet |
pass relevant options from "sledgehammer" to "sledgehammer minimize";
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 18:44:12 +0200 |
blanchet |
get rid of "conjecture_pos", which is no longer necessary now that it's Metis's job, not Sledgehammer's, to report inconsistent contexts
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 15:24:57 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 15:15:21 +0200 |
blanchet |
make Sledgehammer's minimizer also minimize Isar proofs
|
file |
diff |
annotate
|
| Wed, 14 Apr 2010 16:50:25 +0200 |
blanchet |
fixed handling of "sledgehammer_params" that get a default value from Isabelle menu;
|
file |
diff |
annotate
|
| Thu, 01 Apr 2010 10:26:45 +0200 |
blanchet |
fixed layout of Sledgehammer output
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 19:49:57 +0200 |
blanchet |
added "modulus" and "sorts" options to control Sledgehammer's Isar proof output
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 18:44:24 +0200 |
blanchet |
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 12:30:33 +0100 |
blanchet |
honor the newly introduced Sledgehammer parameters and fixed the parsing;
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 11:39:21 +0100 |
blanchet |
added options to Sledgehammer;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 10:25:07 +0100 |
blanchet |
start work on direct proof reconstruction for Sledgehammer
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 16:04:15 +0100 |
blanchet |
renamed "e_full" and "vampire_full" to "e_isar" and "vampire_isar";
|
file |
diff |
annotate
|