| 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:27:53 +0200 |
blanchet |
exploit "Name.desymbolize" to remove some dependencies
|
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
|
| Fri, 25 Jun 2010 15:22:12 +0200 |
blanchet |
got rid of needless exception
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 23:54:02 +0200 |
blanchet |
factor out TPTP format output into file of its own, to facilitate further changes
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 16:23:29 +0200 |
blanchet |
thread original theorem along with CNF theorem, as a step toward killing the Skolem cache
|
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 16:43:44 +0200 |
blanchet |
expect SPASS 3.7, and give a friendly warning if an older version is used
|
file |
diff |
annotate
|
| Mon, 17 May 2010 10:18:14 +0200 |
blanchet |
generate proper arity declarations for TFrees for SPASS's DFG format;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
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
|
| Wed, 28 Apr 2010 16:03:49 +0200 |
blanchet |
reintroduced short names for HOL->FOL constants; other parts of the code rely on these
|
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
|
| Tue, 27 Apr 2010 14:27:47 +0200 |
blanchet |
in Sledgehammer "debug" mode, the names of most variables are already short and sweet, so most of the entries of the "const_trans_table" don't have a raison d'etre anymore
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 11:38:46 +0200 |
blanchet |
support readable names even when Isar proof reconstruction is enabled -- useful for debugging
|
file |
diff |
annotate
|
| Fri, 23 Apr 2010 19:12:49 +0200 |
blanchet |
remove some bloat
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 11:54:07 +0200 |
blanchet |
don't use readable names if proof reconstruction is needed, because it uses the structure of names
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 11:02:00 +0200 |
blanchet |
allow "_" in TPTP names in debug mode
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 09:53:31 +0200 |
blanchet |
get rid of "List.foldl" + add timestamp to SPASS
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 15:49:13 +0200 |
blanchet |
added original constant names to Sledgehammer internal terms + output short names if "debug" is set (for increased readability)
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 14:48:34 +0200 |
blanchet |
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 13:57:17 +0200 |
blanchet |
give more sensible names to "fol_type" constructors, as requested by a FIXME comment
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 13:49:46 +0200 |
blanchet |
make Sledgehammer's output more debugging friendly
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 18:44:24 +0200 |
blanchet |
make Sledgehammer output "by" vs. "apply", "qed" vs. "next", and any necessary "prefer"
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 15:50:18 +0200 |
blanchet |
get rid of Polyhash, since it's no longer used
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:37:44 +0100 |
blanchet |
renamed "ATP_Linkup" theory to "Sledgehammer"
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 19:26:05 +0100 |
blanchet |
renamed Sledgehammer structures
|
file |
diff |
annotate
|
| Wed, 17 Mar 2010 18:16:31 +0100 |
blanchet |
move Sledgehammer files in a directory of their own
|
file |
diff |
annotate
| base
|