| Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
automatically use "metisFT" when typed helpers are necessary
|
file |
diff |
annotate
|
| Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
more informative message when Sledgehammer finds an unsound proof
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
fixed several bugs in Isar proof reconstruction, in particular w.r.t. mangled types and hAPP
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
no need to use metisFT for Isar proofs -- metis falls back on it anyway
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
robustly detect how many type args were passed to the ATP, even if some of them were omitted
|
file |
diff |
annotate
|
| Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
fixed conjecture resolution bug for Vampire 1.0's TSTP output
|
file |
diff |
annotate
|
| Wed, 04 May 2011 19:35:48 +0200 |
blanchet |
exploit inferred monotonicity
|
file |
diff |
annotate
|
| Tue, 03 May 2011 01:04:03 +0200 |
blanchet |
no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter
|
file |
diff |
annotate
|
| Mon, 02 May 2011 14:40:57 +0200 |
blanchet |
use strings to encode type systems in ATP module, to reduce the amount of out-of-place information and also to make it easier to print the type system used
|
file |
diff |
annotate
|
| Mon, 02 May 2011 12:09:33 +0200 |
blanchet |
show sorts not just types in Isar proofs + tuning
|
file |
diff |
annotate
|
| Mon, 02 May 2011 01:05:24 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Sun, 01 May 2011 22:36:58 +0200 |
blanchet |
use "metis", not "metisFT", to reconstruct proofs found in fully-typed mode -- "metisFT" is just too slow...
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
restructured type systems some more -- the old naming schemes had "argshg diff |less" and "tagshg diff |less" as equivalent and didn't support a monomorphic version of "tags"
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
fixed SPASS fact offset calculation and report unexpected unsound proofs with so-called sound encodings
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
implement the new ATP type system in Sledgehammer
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
cleanup proxification/unproxification and make sure that "num_atp_type_args" is called on the proxy in the reconstruction code, since "c_fequal" has one type arg but the unproxified equal has 0
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
no needless "fequal" proxies if "explicit_apply" is set + always have readable names
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
improve helper type instantiation code
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
killed needless datatype "combtyp" in Metis
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added friendly hint when Isar proof is missing
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
reconstruct TFF type predicates correctly for ToFoF
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
handle special constants correctly in Isar proof reconstruction code, especially type predicates
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
reimplemented the hAPP introduction code so that it's done earlier, when the types are still available
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
move type declarations to the front, for TFF-compliance
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
generate typing for "hBOOL" in "Many_Typed" mode + tuning
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added more rudimentary type support to Sledgehammer's ATP encoding
|
file |
diff |
annotate
|
| Sun, 01 May 2011 18:37:24 +0200 |
blanchet |
added room for types in ATP quantifiers
|
file |
diff |
annotate
|
| Fri, 22 Apr 2011 00:00:05 +0200 |
blanchet |
automatically remove offending facts when faced with an unsound proof -- instead of using the highly inefficient "full_types" option
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 22:18:28 +0200 |
blanchet |
detect some unsound proofs before showing them to the user
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|