| 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
|