| Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
normalize indices in chained facts to make sure that backtick facts (which often result in different names) are recognized + changed definition of urgent messages
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
show time taken for reconstruction
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
use helpers and tweak Quickcheck's priority to it comes second (to give Solve Direct slightly more time before another prover runs)
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
merge timeout messages from several ATPs into one message to avoid clutter
|
file |
diff |
annotate
|
| Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
file |
diff |
annotate
|
| Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
eliminated more code duplication in Nitrox
|
file |
diff |
annotate
|
| Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
improved Waldmeister support -- even run it by default on unit equational goals
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
improved "poly_preds_{bang,query}" by picking up good witnesses for the possible infinity of common type classes and ensuring that "?'a::type" doesn't ruin everything
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
reintroduced type encodings "poly_preds_{bang,query}", but this time being more liberal about type variables of known safe sorts
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
|
file |
diff |
annotate
|
| Thu, 05 May 2011 12:40:48 +0200 |
blanchet |
query typedefs as well for monotonicity
|
file |
diff |
annotate
|
| Wed, 04 May 2011 19:35:48 +0200 |
blanchet |
exploit inferred monotonicity
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 16:34:14 +0200 |
wenzelm |
discontinued special treatment of structure Lexicon;
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:46:54 +0100 |
blanchet |
no need to do a super-duper atomization if Metis fails afterwards anyway
|
file |
diff |
annotate
|
| Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
instantiate induction rules automatically
|
file |
diff |
annotate
|
| Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 22:26:53 +0100 |
blanchet |
standardize on seconds for Nitpick and Sledgehammer timeouts
|
file |
diff |
annotate
|
| Wed, 29 Sep 2010 23:30:10 +0200 |
blanchet |
finished renaming file and module
|
file |
diff |
annotate
|
| Mon, 27 Sep 2010 10:44:08 +0200 |
blanchet |
rename "Clausifier" to "Meson_Clausifier" and merge with "Meson_Tactic"
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 15:08:51 +0200 |
wenzelm |
added XML.content_of convenience -- cover XML.body, which is the general situation;
|
file |
diff |
annotate
|
| Fri, 17 Sep 2010 01:22:01 +0200 |
blanchet |
move functions around
|
file |
diff |
annotate
|
| Thu, 16 Sep 2010 14:24:48 +0200 |
blanchet |
avoid code duplication
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 11:18:40 +0200 |
blanchet |
speed up helper function
|
file |
diff |
annotate
|
| Sat, 11 Sep 2010 10:21:52 +0200 |
blanchet |
implemented Auto Sledgehammer
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 14:05:22 +0200 |
blanchet |
improve SPASS hack, when a clause comes from several facts
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 10:42:06 +0200 |
blanchet |
consider "locality" when assigning weights to facts
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 22:57:22 +0200 |
blanchet |
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 18:03:43 +0200 |
blanchet |
clean handling of whether a fact is chained or not;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 16:24:11 +0200 |
blanchet |
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
|
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
|
| Fri, 20 Aug 2010 10:58:01 +0200 |
blanchet |
beta eta contract the Sledgehammer conjecture (and also the axioms, although this might not be needed), just like Metis does (implicitly);
|
file |
diff |
annotate
|
| Thu, 05 Aug 2010 12:40:12 +0200 |
blanchet |
fix bug in Nitpick's "equationalize" function (the prems were ignored) + make it do some basic extensionalization
|
file |
diff |
annotate
|
| Wed, 28 Jul 2010 18:54:18 +0200 |
blanchet |
minor refactoring
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 17:43:11 +0200 |
blanchet |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:03:21 +0200 |
blanchet |
generate full first-order formulas (FOF) in Sledgehammer
|
file |
diff |
annotate
|
| Fri, 23 Jul 2010 21:29:29 +0200 |
blanchet |
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 16:27:53 +0200 |
blanchet |
exploit "Name.desymbolize" to remove some dependencies
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 14:28:22 +0200 |
blanchet |
removed Sledgehammer's support for the DFG syntax;
|
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
|
| Wed, 02 Jun 2010 15:18:48 +0200 |
blanchet |
honor "xsymbols"
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
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 16:14:56 +0200 |
blanchet |
parentheses around nested cases
|
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 12:46:50 +0200 |
blanchet |
support Vampire definitions of constants as "let" constructs in Isar proofs
|
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
|
| 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
|
| Fri, 23 Apr 2010 19:12:49 +0200 |
blanchet |
remove some bloat
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 16:13:49 +0200 |
blanchet |
Sledgehammer: the empty set of fact () should mean nothing, not unchanged
|
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
|
| Wed, 14 Apr 2010 18:23:51 +0200 |
blanchet |
make Sledgehammer "minimize" output less confusing + round up (not down) time limits to nearest second
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 15:50:18 +0200 |
blanchet |
get rid of Polyhash, since it's no longer used
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 11:39:21 +0100 |
blanchet |
added options to Sledgehammer;
|
file |
diff |
annotate
|