| Sat, 20 Sep 2014 10:44:24 +0200 |
steckerm |
Minor fixes in ATP_Waldmeister
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:44:23 +0200 |
steckerm |
Made encoded type for apply less restrictive
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:44:23 +0200 |
steckerm |
Updated fix_name function
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Added support for partial function application
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Improved equality handling in skolemization
|
file |
diff |
annotate
|
| Sat, 20 Sep 2014 10:42:08 +0200 |
steckerm |
Re-added hypothesis argument to problem generation
|
file |
diff |
annotate
|
| Sun, 07 Sep 2014 14:39:23 +0200 |
steckerm |
Added translation for lambda expressions in terms.
|
file |
diff |
annotate
|
| Tue, 02 Sep 2014 16:38:26 +0200 |
steckerm |
Some work on the new waldmeister integration
|
file |
diff |
annotate
|
| Wed, 30 Jul 2014 00:50:41 +0200 |
blanchet |
also try 'metis' with 'full_types'
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
more robust handling of types for skolems (modeled as Frees)
|
file |
diff |
annotate
|
| Tue, 17 Jun 2014 18:33:34 +0200 |
blanchet |
reintroduce atomize in Waldmeister code
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:42:44 +0200 |
blanchet |
integrated new Waldmeister code with 'sledgehammer' command
|
file |
diff |
annotate
|
| Mon, 16 Jun 2014 19:40:04 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
| base
|