| Tue, 24 Aug 2010 15:29:13 +0200 |
blanchet |
revert this idea of automatically invoking "metisFT" when "metis" fails;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 14:54:17 +0200 |
blanchet |
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 14:27:30 +0200 |
blanchet |
treat "using X by metis" (more or less) the same as "by (metis X)"
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 15:56:00 +0200 |
blanchet |
temporarily disable "fequal" handling in Metis;
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 14:18:55 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 18:16:47 +0200 |
blanchet |
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 11:02:14 +0200 |
haftmann |
use antiquotations for remaining unqualified constants in HOL
|
file |
diff |
annotate
|
| Mon, 16 Aug 2010 09:39:05 +0200 |
blanchet |
Geoff's formatter now needs closed formulas
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 11:03:54 +0200 |
blanchet |
replace recursion with "fold"
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 22:43:46 +0200 |
blanchet |
use "explicit_apply" in the minimizer whenever it might make a difference to prevent freak failures;
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 22:13:15 +0200 |
blanchet |
fix Meson's definition of first-orderness to prevent errors later on elsewhere (e.g. in Metis)
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 20:15:50 +0200 |
blanchet |
revert exception throwing in FOL_SOLVE, since they're not caught anyway
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 19:41:19 +0200 |
blanchet |
minor refactoring
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 19:17:15 +0200 |
blanchet |
standardize "Author" tags
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 17:15:12 +0200 |
blanchet |
get rid of more dead wood
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 14:14:24 +0200 |
blanchet |
make TPTP generator accept full first-order formulas
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 11:21:25 +0200 |
blanchet |
renamed internal function
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:15:49 +0200 |
blanchet |
revert code that was submitted by mistake
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:15:07 +0200 |
blanchet |
renamings + only need second component of name pool to reconstruct proofs
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:14:47 +0200 |
blanchet |
rename "classrel" to "class_rel"
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:14:26 +0200 |
blanchet |
rename "combtyp" constructors
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:14:07 +0200 |
blanchet |
renamed "Literal" to "FOLLiteral"
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 18:03:34 +0200 |
blanchet |
rewrote the TPTP problem generation code more or less from scratch;
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 11:29:31 +0200 |
blanchet |
move function
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 10:56:45 +0200 |
blanchet |
Sledgehammer can save some msecs by cheating
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 10:25:53 +0200 |
blanchet |
move blacklisting completely out of the clausifier;
|
file |
diff |
annotate
|
| 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:08:36 +0200 |
blanchet |
killed "expand_defs_tac";
|
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 16:03:34 +0200 |
blanchet |
fewer dependencies
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 15:59:13 +0200 |
blanchet |
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 15:01:35 +0200 |
blanchet |
move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 21:00:37 +0200 |
blanchet |
make sure "metisFT" is tried upon "metis" failure in "resolve_inc_tyvars"
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 10:38:01 +0200 |
blanchet |
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 14:36:23 +0200 |
blanchet |
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
|
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 14:28:22 +0200 |
blanchet |
removed Sledgehammer's support for the DFG syntax;
|
file |
diff |
annotate
|
| Mon, 21 Jun 2010 12:31:41 +0200 |
blanchet |
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 20:16:36 +0200 |
blanchet |
A function called "untyped_aconv" shouldn't look at the bound names!
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 10:36:01 +0200 |
blanchet |
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
|
file |
diff |
annotate
|
| Sat, 12 Jun 2010 11:11:07 +0200 |
blanchet |
"raise Fail" for internal errors + one new internal error (instead of "Match")
|
file |
diff |
annotate
|
| Fri, 11 Jun 2010 17:10:23 +0200 |
blanchet |
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 12:28:42 +0200 |
blanchet |
give more helpful error message
|
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
|
| Mon, 17 May 2010 10:18:14 +0200 |
blanchet |
generate proper arity declarations for TFrees for SPASS's DFG format;
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
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
|
| 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
|
| Mon, 26 Apr 2010 21:18:20 +0200 |
blanchet |
adapt code to reflect new signature of "neg_clausify"
|
file |
diff |
annotate
|
| Sat, 24 Apr 2010 16:05:42 +0200 |
blanchet |
better error reporting;
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 18:14:45 +0200 |
blanchet |
added warning about inconsistent context to Metis;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 15:49:13 +0200 |
blanchet |
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 14:48:34 +0200 |
blanchet |
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 13:57:17 +0200 |
blanchet |
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
|
file |
diff |
annotate
|
| Sun, 28 Mar 2010 16:59:06 +0200 |
wenzelm |
static defaults for configuration options;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:26:05 +0100 |
blanchet |
renamed Sledgehammer structures
|
file |
diff |
annotate
|