Mon, 12 Sep 2011 10:49:37 +0200 |
blanchet |
fixed type intersection (again)
|
file |
diff |
annotate
|
Sat, 10 Sep 2011 00:44:25 +0200 |
blanchet |
fixed definition of type intersection (soundness bug)
|
file |
diff |
annotate
|
Wed, 07 Sep 2011 13:50:17 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 22:06:25 +0200 |
blanchet |
make default unsound mode less unsound
|
file |
diff |
annotate
|
Thu, 25 Aug 2011 14:25:06 +0200 |
blanchet |
fixed bang encoding detection of which types to encode
|
file |
diff |
annotate
|
Wed, 24 Aug 2011 11:17:33 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
added caching for (in)finiteness checks
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
make sound mode more sound (and clean up code)
|
file |
diff |
annotate
|
Mon, 22 Aug 2011 15:02:45 +0200 |
blanchet |
reintroduced slightly unsound optimization taken out in 717880e98e6b, but only if "sound" is false
|
file |
diff |
annotate
|
Sun, 17 Jul 2011 14:21:19 +0200 |
blanchet |
fixed lambda-liftg: must ensure the formulas are in close form
|
file |
diff |
annotate
|
Sun, 17 Jul 2011 14:12:45 +0200 |
blanchet |
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
|
Thu, 14 Jul 2011 16:50:05 +0200 |
blanchet |
added option to control which lambda translation to use (for experiments)
|
file |
diff |
annotate
|
Mon, 27 Jun 2011 14:56:28 +0200 |
blanchet |
added "sound" option to force Sledgehammer to be pedantically sound
|
file |
diff |
annotate
|
Thu, 16 Jun 2011 13:50:35 +0200 |
blanchet |
gave up an optimization that sometimes lead to unsound proofs -- in short, facts talking about a schematic type variable can encode a cardinality constraint and be consistent with HOL, e.g. "card (UNIV::?'a set) = 1 ==> ALL x y. x = y"
|
file |
diff |
annotate
|
Mon, 06 Jun 2011 20:36:35 +0200 |
blanchet |
gracefully handle the case where a constant is partially or not instantiated at all, as may happen when reconstructing Metis proofs for polymorphic type encodings
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
|