| Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
more through tests of new Metis
|
file |
diff |
annotate
|
| Wed, 01 Jun 2011 00:12:38 +0200 |
blanchet |
make sure "Trueprop" is removed before combinators are added -- the code is fragile in that respect
|
file |
diff |
annotate
|
| Tue, 31 May 2011 23:39:27 +0200 |
blanchet |
speed up example by disabling preplay, and temporarily comment out a broken Sledgehammer call
|
file |
diff |
annotate
|
| Fri, 20 May 2011 18:12:12 +0200 |
blanchet |
update example
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:59:33 +0200 |
blanchet |
exercise more type systems (but only sound or quasi-sound ones)
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
another concession to backward compatibility
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
handle equality proxy in a more backward-compatible way
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
added two mildly higher-order examples contributed by TN, removed references to obsoleted type systems, and moved things around
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
renamed type systems for more consistency
|
file |
diff |
annotate
|
| Wed, 04 May 2011 23:21:11 +0200 |
blanchet |
compile + added monotonicity tests
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:52:38 +0200 |
blanchet |
adapt to new type system names
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
use new type system syntax
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
more higher-order tests for Sledgehammer/ATP
|
file |
diff |
annotate
|
| Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
Metis examples use the new Skolemizer to test it
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
improve partially tagged encoding by adding a helper fact that coalesces consecutive "ti" tags
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
example tuning
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added example to exercise higher-order reasoning with Sledgehammer and Metis
|
file |
diff |
annotate
|