| Thu, 19 Jan 2012 21:37:12 +0100 |
renamed "sound" option to "strict"
|
file | diff | annotate |
| Fri, 18 Nov 2011 11:47:12 +0100 |
removed needless baggage
|
file | diff | annotate |
| Tue, 15 Nov 2011 22:13:39 +0100 |
started implementing lambda-lifting in Metis
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:51:35 +0200 |
also export DFG formats
|
file | diff | annotate |
| Sat, 29 Oct 2011 13:15:58 +0200 |
added sorted DFG output for coming version of SPASS
|
file | diff | annotate |
| Mon, 19 Sep 2011 23:34:22 +0200 |
fixed headers;
|
file | diff | annotate |
| Wed, 31 Aug 2011 08:49:10 +0200 |
killed FIXME (the ATP exporter outputs TPTP FOF, which is first-order)
|
file | diff | annotate |
| Tue, 30 Aug 2011 14:12:55 +0200 |
improved handling of induction rules in Sledgehammer
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
cleaner handling of polymorphic monotonicity inference
|
file | diff | annotate |
| Mon, 22 Aug 2011 15:02:45 +0200 |
added option to control soundness of encodings more precisely, for evaluation purposes
|
file | diff | annotate |
| Tue, 09 Aug 2011 09:05:22 +0200 |
move lambda-lifting code to ATP encoding, so it can be used by Metis
|
file | diff | annotate |
| Thu, 28 Jul 2011 11:49:03 +0200 |
clean up temporary directory hack
|
file | diff | annotate |
| Thu, 28 Jul 2011 11:43:45 +0200 |
make SML/NJ happy
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:12:45 +0200 |
ensure that the lambda translation procedure is called only once with all the facts, which is necessary for soundness of lambda-lifting (freshness of new names)
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:11:35 +0200 |
pass kind to lambda-translation function
|
file | diff | annotate |
| Sun, 17 Jul 2011 14:11:34 +0200 |
move more lambda-handling logic to Sledgehammer, from ATP module, for formal dependency reasons
|
file | diff | annotate |
| Sat, 16 Jul 2011 20:52:41 +0200 |
moved bash operations to Isabelle_System (cf. Scala version);
|
file | diff | annotate |
| Thu, 14 Jul 2011 16:50:05 +0200 |
move lambda translation option from ATP to Sledgehammer, to avoid accidentally breaking Metis (its reconstruction code can only deal with combinators)
|
file | diff | annotate |
| Wed, 13 Jul 2011 22:16:19 +0200 |
cleanly separate TPTP related files from other examples
|
file | diff | annotate | base |