| Mon, 20 Sep 2010 11:51:19 +0200 |
blanchet |
merge tracing of two related modules
|
file |
diff |
annotate
|
| Sat, 18 Sep 2010 10:43:52 +0200 |
blanchet |
preprocess "All" before doing clausification in Metis;
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 17:30:29 +0200 |
blanchet |
complete refactoring of Metis along the lines of Sledgehammer
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 16:12:02 +0200 |
blanchet |
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 08:29:50 +0200 |
blanchet |
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 16:23:11 +0200 |
blanchet |
"Metis." -> "Metis_" to reflect change in "metis.ML"
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 23:38:20 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 11:07:23 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 21:23:09 +0200 |
blanchet |
adapt to latest Metis version
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 20:11:52 +0200 |
blanchet |
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 18:53:55 +0200 |
blanchet |
clarify comment
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 18:50:23 +0200 |
blanchet |
improve on 65903ec4e8e8: fix more "add_ffpair" exceptions in failed ATP proofs
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 14:47:06 +0200 |
blanchet |
add cutoff beyond which facts are handled using definitional CNF
|
file |
diff |
annotate
|
| Wed, 08 Sep 2010 19:22:37 +0200 |
blanchet |
workaround to avoid subtle "add_ffpairs" unification exception in Sledgehammer;
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 14:20:47 +0200 |
blanchet |
remove code I submitted accidentally
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 13:54:04 +0200 |
blanchet |
disable "definitional CNF";
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 13:45:23 +0200 |
blanchet |
FIXME -> TODO (nothing is broken)
|
file |
diff |
annotate
|
| Thu, 02 Sep 2010 13:18:19 +0200 |
blanchet |
Let MESON take an additional "preskolemization tactic", which can be used to put the goal in definitional CNF
|
file |
diff |
annotate
|
| Wed, 01 Sep 2010 11:59:04 +0200 |
blanchet |
fiddled with fudge factor (based on Mirabelle)
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 00:49:38 +0200 |
blanchet |
renaming
|
file |
diff |
annotate
|
| 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
|