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
|
Mon, 04 Apr 2011 18:53:35 +0200 |
blanchet |
if "monomorphize" is enabled, mangle the type information in the names by default
|
file |
diff |
annotate
|
Thu, 31 Mar 2011 11:16:52 +0200 |
blanchet |
added monomorphization option to Sledgehammer ATPs -- this looks promising but is still off by default
|
file |
diff |
annotate
|
Wed, 09 Feb 2011 17:18:58 +0100 |
blanchet |
automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices)
|
file |
diff |
annotate
|
Thu, 16 Dec 2010 15:12:17 +0100 |
blanchet |
fixed more issues with the Vampire output parser, and added support for Vampire's TSTP output (--proof tptp)
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 11:26:29 +0100 |
blanchet |
generate a "using [[smt_solver = ...]]" command if a proof is found by another SMT solver than the current one, to ensure it's also used for reconstruction
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
fix Vampire parsing problem
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
added Sledgehammer support for higher-order propositional reasoning
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
implemented partially-typed "tags" type encoding
|
file |
diff |
annotate
|
Wed, 15 Dec 2010 11:26:28 +0100 |
blanchet |
implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound
|
file |
diff |
annotate
|
Fri, 26 Nov 2010 22:22:07 +0100 |
blanchet |
put facts found by SMT solver in alphabetical order and omit chained facts, as was done already for ATP proofs
|
file |
diff |
annotate
|
Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
file |
diff |
annotate
|
Tue, 26 Oct 2010 21:01:28 +0200 |
blanchet |
standardize on "fact" terminology (vs. "axiom" or "theorem") in Sledgehammer -- but keep "Axiom" in the lower-level "ATP_Problem" module
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 18:31:45 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 16:45:55 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 14:10:32 +0200 |
blanchet |
fixed signature of "is_smt_solver_installed";
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 13:57:54 +0200 |
blanchet |
renamed modules
|
file |
diff |
annotate
|
Fri, 22 Oct 2010 13:54:51 +0200 |
blanchet |
renamed files
|
file |
diff |
annotate
| base
|