| Mon, 20 Sep 2010 16:31:47 +0200 |
blanchet |
remove needless exception
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 23:38:20 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 14 Sep 2010 09:12:28 +0200 |
blanchet |
rename internal Sledgehammer constant
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 20:09:43 +0200 |
blanchet |
use the Meson cutoff as the cutoff for using definitional CNF -- it's simpler that way
|
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
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Fri, 03 Sep 2010 13:54:04 +0200 |
blanchet |
disable "definitional CNF";
|
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
|
| Thu, 02 Sep 2010 11:29:02 +0200 |
blanchet |
use definitional CNFs in Metis rather than plain CNF, following a suggestion by Joe Hurd;
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
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 14:09:02 +0200 |
blanchet |
transform elim theorems before filtering "bool" and "prop" variables out;
|
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
|
| Mon, 09 Aug 2010 12:05:48 +0200 |
blanchet |
move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML)
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 11:03:54 +0200 |
blanchet |
replace recursion with "fold"
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 10:38:57 +0200 |
blanchet |
remove now needless "Thm.transfer"
|
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 23:54:40 +0200 |
blanchet |
prevent schematic variable clash in combinator-introduction code, when invoked from Sledgehammer (another consequence of the CNF -> FOF transition)
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 20:07:31 +0200 |
blanchet |
reintroduced more preprocessing steps to Sledgehammer, adapted to the new FOF setting
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:56:10 +0200 |
blanchet |
added extensionalization to Sledgehammer, mimicking what the Clausifier used to do
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:03:21 +0200 |
blanchet |
generate full first-order formulas (FOF) in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 11:03:26 +0200 |
blanchet |
more elegant cheating
|
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
|
| Mon, 28 Jun 2010 18:15:40 +0200 |
blanchet |
remove obsolete component of CNF clause tuple (and reorder it)
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 18:02:36 +0200 |
blanchet |
get rid of Skolem cache by performing CNF-conversion after fact selection
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 17:32:28 +0200 |
blanchet |
always perform "inline" skolemization, polymorphism or not, Skolem cache or not
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 17:31:38 +0200 |
blanchet |
always perform relevance filtering on original formulas
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 18:34:06 +0200 |
blanchet |
factor out thread creation
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 16:15:03 +0200 |
blanchet |
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
|
file |
diff |
annotate
| base
|