| Wed, 28 Jul 2010 10:06:06 +0200 |
blanchet |
support latest version of Vampire (1.0) locally
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 19:41:19 +0200 |
blanchet |
minor refactoring
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 19:17:15 +0200 |
blanchet |
standardize "Author" tags
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 17:43:11 +0200 |
blanchet |
complete renaming of "Sledgehammer_TPTP_Format" to "ATP_Problem"
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 17:32:10 +0200 |
blanchet |
move Sledgehammer-specific code out of "Sledgehammer_TPTP_Format"
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 17:04:09 +0200 |
blanchet |
implemented "sublinear" minimization algorithm
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 15:28:23 +0200 |
blanchet |
extract sort constraints from FOFs properly;
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 12:01:02 +0200 |
blanchet |
handle Vampire's equality proxy axiom correctly
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:22:39 +0200 |
blanchet |
remove more Skolemization-aware code
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:09:10 +0200 |
blanchet |
simplify "conjecture_shape" business, as a result of using FOF instead of CNF
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:03:21 +0200 |
blanchet |
generate full first-order formulas (FOF) in Sledgehammer
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 14:14:24 +0200 |
blanchet |
make TPTP generator accept full first-order formulas
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 11:21:11 +0200 |
blanchet |
proof reconstruction for full FOF terms
|
file |
diff |
annotate
|
| Fri, 23 Jul 2010 21:29:29 +0200 |
blanchet |
keep track of clause numbers for SPASS now that we generate FOF rather than CNF problems;
|
file |
diff |
annotate
|
| Fri, 23 Jul 2010 15:04:49 +0200 |
blanchet |
first step in using "fof" rather than "cnf" in TPTP problems
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 21:15:07 +0200 |
blanchet |
renamings + only need second component of name pool to reconstruct proofs
|
file |
diff |
annotate
|
| Wed, 30 Jun 2010 18:03:34 +0200 |
blanchet |
rewrote the TPTP problem generation code more or less from scratch;
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 09:19:16 +0200 |
blanchet |
move "nice names" from Metis to TPTP format
|
file |
diff |
annotate
|
| Mon, 28 Jun 2010 17:31:38 +0200 |
blanchet |
always perform relevance filtering on original formulas
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 17:08:39 +0200 |
blanchet |
renamed "Sledgehammer_FOL_Clauses" to "Metis_Clauses", so that Metis doesn't depend on Sledgehammer
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 16:42:06 +0200 |
blanchet |
merge "Sledgehammer_{F,H}OL_Clause", as requested by a FIXME
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 16:15:03 +0200 |
blanchet |
renamed "Sledgehammer_Fact_Preprocessor" to "Clausifier";
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 15:59:13 +0200 |
blanchet |
more intra-module dependency cleanup + merge "const" and "type_const" tables, since this is safe
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 14:28:22 +0200 |
blanchet |
removed Sledgehammer's support for the DFG syntax;
|
file |
diff |
annotate
|
| Mon, 21 Jun 2010 12:31:41 +0200 |
blanchet |
try to improve Sledgehammer/Metis's behavior in full_types mode, e.g. by handing True, False, and If better
|
file |
diff |
annotate
|
| Mon, 14 Jun 2010 10:36:01 +0200 |
blanchet |
adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf"
|
file |
diff |
annotate
|
| Fri, 11 Jun 2010 17:10:23 +0200 |
blanchet |
proper polymorphic Skolemization of uncached facts + synchronization of caching and relevance filter
|
file |
diff |
annotate
|
| Fri, 04 Jun 2010 14:08:23 +0200 |
blanchet |
fix bugs in Sledgehammer's Isar proof "redirection" code
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 17:19:44 +0200 |
blanchet |
handle Vampire's definitions smoothly
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 17:06:28 +0200 |
blanchet |
fix bug in direct Isar proofs, which was exhibited by the "BigO" example
|
file |
diff |
annotate
|
| Wed, 02 Jun 2010 14:35:52 +0200 |
blanchet |
show types in Isar proofs, but not for free variables;
|
file |
diff |
annotate
|
| Fri, 28 May 2010 17:00:38 +0200 |
blanchet |
merged
|
file |
diff |
annotate
|
| Fri, 28 May 2010 13:49:21 +0200 |
blanchet |
make sure chained facts appear in Isar proofs generated by Sledgehammer -- otherwise the proof won't work
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:10:37 +0200 |
wenzelm |
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:21:11 +0200 |
blanchet |
make sure chained facts don't pop up in the metis proof
|
file |
diff |
annotate
|
| Mon, 17 May 2010 12:15:37 +0200 |
blanchet |
fix bug in Isar proof reconstruction step relabeling + don't try to infer the sorts of TVars, since this often fails miserably
|
file |
diff |
annotate
|
| Fri, 14 May 2010 22:29:50 +0200 |
blanchet |
renamed options
|
file |
diff |
annotate
|
| Fri, 14 May 2010 11:23:42 +0200 |
blanchet |
made Sledgehammer's full-typed proof reconstruction work for the first time;
|
file |
diff |
annotate
|
| Sat, 01 May 2010 21:29:03 +0200 |
krauss |
made sml/nj happy about Sledgehammer and Nitpick (cf. 6f11c9b1fb3e, 3c2438efe224)
|
file |
diff |
annotate
|
| Sat, 01 May 2010 20:49:39 +0200 |
krauss |
Backed out changeset 6f11c9b1fb3e (breaks compilation of HOL image)
|
file |
diff |
annotate
|
| Sat, 01 May 2010 10:37:31 +0200 |
blanchet |
now if this doesn't make SML/NJ happy, nothing will
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 14:52:49 +0200 |
blanchet |
eliminate trivial case splits from Isar proofs
|
file |
diff |
annotate
|
| Fri, 30 Apr 2010 13:58:35 +0200 |
blanchet |
identify axioms/conjectures more reliably in ATP proofs (an empty dependency list doesn't always indicate an axiom or conjecture!)
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 19:07:36 +0200 |
blanchet |
uncomment code
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:45:39 +0200 |
blanchet |
be more discriminate: some one-line Isar proofs are silly
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:39:46 +0200 |
blanchet |
one-step Isar proofs are not always pointless
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 17:31:08 +0200 |
blanchet |
the SPASS output syntax is more general than I thought -- such a pity that there's no documentation
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 12:21:20 +0200 |
blanchet |
fixed definition of "bad frees" so that it actually works
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 11:38:23 +0200 |
blanchet |
don't remove last line of proof
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 11:22:24 +0200 |
blanchet |
handle previously unknown SPASS syntaxes in Sledgehammer's proof reconstruction
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 10:55:59 +0200 |
blanchet |
make SML/NJ happy, take 2
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 10:25:26 +0200 |
blanchet |
use readable names in "debug" mode for type vars + don't pipe facts using "using" but rather give them directly to metis (works better with type variables)
|
file |
diff |
annotate
|
| Thu, 29 Apr 2010 01:17:14 +0200 |
blanchet |
expand combinators in Isar proofs constructed by Sledgehammer;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 21:59:29 +0200 |
blanchet |
improve unskolemization
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 17:47:30 +0200 |
blanchet |
try out Vampire 11 and parse its output correctly;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 15:53:17 +0200 |
blanchet |
save the name of Skolemized variables in Sledgehammer for use in the proof reconstruction code
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 15:34:55 +0200 |
blanchet |
unskolemize formulas in proof reconstruction + detect newer SPASS versions to avoid truncating identifiers if not necessary (truncating confuses proof reconstruction)
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 13:00:30 +0200 |
blanchet |
remove Sledgehammer's "sorts" option to annotate variables with sorts in proof;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 12:46:50 +0200 |
blanchet |
support Vampire definitions of constants as "let" constructs in Isar proofs
|
file |
diff |
annotate
|