Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new Metis
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
more work on new metis that exploits the powerful new type encodings
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
removed obscure option
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
added new metis mode, with no implementation yet
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
tuning
|
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
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
cleaner handling of equality and proxies (esp. for THF)
|
file |
diff |
annotate
|
Fri, 20 May 2011 18:01:46 +0200 |
blanchet |
name tuning
|
file |
diff |
annotate
|
Fri, 20 May 2011 17:16:13 +0200 |
blanchet |
further improvements to "poly_{preds,tags}_{bang,query}" -- better solution to the combinator problem + make sure type assumptions can be discharged
|
file |
diff |
annotate
|
Fri, 20 May 2011 17:16:13 +0200 |
blanchet |
prevent unsound combinator proofs in partially typed polymorphic type systems
|
file |
diff |
annotate
|
Fri, 20 May 2011 12:47:58 +0200 |
blanchet |
tuning
|
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 |
reenabled equality proxy in Metis for higher-order reasoning
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
ensure type class predicates are generated in symbol declarations (for "poly_preds" and similar)
|
file |
diff |
annotate
|
Tue, 03 May 2011 14:23:40 +0200 |
blanchet |
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
|
file |
diff |
annotate
|
Sun, 01 May 2011 18:37:25 +0200 |
blanchet |
drop "fequal" type args for unmangled type systems
|
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 |
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 |
have properly type-instantiated helper facts (combinators and If)
|
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 |
no point in keeping indices in Sledgehammer readable var names, since these are disambiguated anyway
|
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
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Thu, 14 Apr 2011 11:24:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
clean up new Skolemizer code -- some old hacks are no longer necessary
|
file |
diff |
annotate
|
Thu, 24 Mar 2011 17:49:27 +0100 |
blanchet |
more robust handling of variables in new Skolemizer
|
file |
diff |
annotate
|