| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
file |
diff |
annotate
|
| Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
use the same code for extensionalization in Metis and Sledgehammer and generalize that code so that it gracefully handles negations (e.g. negated conjecture), formulas of the form (%x. t) = u, etc.
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
added unfold set constant functionality to Meson/Metis -- disabled by default for now
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
more robust exception handling in Metis (also works if there are several subgoals)
|
file |
diff |
annotate
|
| Tue, 03 May 2011 14:23:40 +0200 |
blanchet |
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
|
file |
diff |
annotate
|
| Mon, 02 May 2011 16:33:21 +0200 |
wenzelm |
added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory;
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added a hint to Metis errors suggesting metisFT -- it sometimes work
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
removed obsolete Skolem counter in new Skolemizer
|
file |
diff |
annotate
|
| Thu, 14 Apr 2011 11:24:04 +0200 |
blanchet |
improve definitional CNF on goal by moving "not" past the quantifiers
|
file |
diff |
annotate
|
| Tue, 23 Nov 2010 18:26:56 +0100 |
blanchet |
added "verbose" option to Metis to shut up its warnings if necessary
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
ensure that MESON correctly preserves the name of variables (needed by the new Skolemizer)
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 12:49:05 +0200 |
blanchet |
prevent type errors because of inconsistent skolem Var types by giving fresh indices to Skolems
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:10:00 +0200 |
blanchet |
renaming
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 18:03:18 +0700 |
blanchet |
added "trace_meson" configuration option, replacing old-fashioned reference
|
file |
diff |
annotate
|
| Mon, 11 Oct 2010 18:02:14 +0700 |
blanchet |
added "trace_metis" configuration option, replacing old-fashioned references
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 17:56:41 +0200 |
blanchet |
move code from "Metis_Tactics" to "Metis_Reconstruct"
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 17:42:57 +0200 |
blanchet |
get rid of function that duplicates existing Pure functionality
|
file |
diff |
annotate
|
| Wed, 06 Oct 2010 12:01:55 +0200 |
blanchet |
added a few FIXMEs
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 12:50:45 +0200 |
blanchet |
tuned comments
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:45:10 +0200 |
blanchet |
hide uninteresting MESON/Metis constants and facts and remove "meson_" prefix to (now hidden) fact names
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 11:14:56 +0200 |
blanchet |
clean up debugging output
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 10:59:12 +0200 |
blanchet |
got rid of overkill "meson_choice" attribute;
|
file |
diff |
annotate
|
| Mon, 04 Oct 2010 22:45:09 +0200 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
| base
|