| Thu, 26 Aug 2010 16:18:40 +0200 |
blanchet |
add nameless chained facts to the pool of things known to Sledgehammer
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 14:58:45 +0200 |
blanchet |
if the goal contains no constants or frees, fall back on chained facts, then on local facts, etc., instead of generating a trivial ATP problem
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 14:05:22 +0200 |
blanchet |
improve SPASS hack, when a clause comes from several facts
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 11:51:06 +0200 |
blanchet |
lower penalty for Skolem constants
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 10:56:46 +0200 |
haftmann |
formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 20:51:17 +0200 |
haftmann |
formerly unnamed infix impliciation now named HOL.implies
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 10:42:06 +0200 |
blanchet |
consider "locality" when assigning weights to facts
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 09:23:21 +0200 |
blanchet |
add a bonus for chained facts, since they are likely to be relevant;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 01:03:08 +0200 |
blanchet |
add a penalty for lambda-abstractions;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 00:49:04 +0200 |
blanchet |
fiddle with relevance filter
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 19:41:18 +0200 |
blanchet |
reorganize options regarding to the relevance threshold and decay
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 17:49:52 +0200 |
blanchet |
make relevance filter work in term of a "max_relevant" option + use Vampire SOS;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:42:28 +0200 |
blanchet |
simplify more code
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:34:28 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:32:43 +0200 |
blanchet |
get rid of "defs_relevant" feature;
|
file |
diff |
annotate
|
| Wed, 25 Aug 2010 09:02:07 +0200 |
blanchet |
renamed "relevance_convergence" to "relevance_decay"
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 22:57:22 +0200 |
blanchet |
make sure that "undo_ascii_of" is the inverse of "ascii_of", also for non-printable characters -- and avoid those in ``-style facts
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 19:19:28 +0200 |
blanchet |
compute names lazily;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 18:03:43 +0200 |
blanchet |
clean handling of whether a fact is chained or not;
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 16:43:52 +0200 |
blanchet |
don't backtick facts that contain schematic variables, since this doesn't work (for some reason)
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 16:24:11 +0200 |
blanchet |
quote facts whose names collide with a keyword or command name (cf. "subclass" in "Jinja/J/TypeSafe.thy")
|
file |
diff |
annotate
|
| Tue, 24 Aug 2010 15:07:54 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 23:32:11 +0200 |
blanchet |
cosmetics
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 23:24:24 +0200 |
blanchet |
optimize fact filter some more
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 23:00:57 +0200 |
blanchet |
cache previous iteration's weights, and keep track of what's dirty and what's clean;
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 21:55:52 +0200 |
blanchet |
modified relevance filter
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 18:53:11 +0200 |
blanchet |
invert semantics of "relevance_convergence", to make it more intuitive
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 18:39:12 +0200 |
blanchet |
if no facts were selected on first iteration, try again with a lower threshold
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 18:25:49 +0200 |
blanchet |
weed out junk in relevance filter
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 18:04:31 +0200 |
blanchet |
no need for "eq" facts -- good old "=" is good enough for us
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 17:49:18 +0200 |
blanchet |
destroy elim rules before checking for finite exhaustive facts
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 14:54:17 +0200 |
blanchet |
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 16:56:05 +0200 |
blanchet |
don't penalize abstractions in relevance filter + support nameless `foo`-style facts
|
file |
diff |
annotate
|
| Sun, 22 Aug 2010 08:26:09 +0200 |
blanchet |
more work on finite axiom detection
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 17:52:26 +0200 |
blanchet |
make sure minimizer facts go through "transform_elim_theorems"
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 16:44:48 +0200 |
blanchet |
unbreak "only" option of Sledgehammer
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 16:22:51 +0200 |
blanchet |
improve "x = A | x = B | x = C"-style axiom detection
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 14:15:29 +0200 |
blanchet |
improve "x = A | x = B | x = C"-style fact discovery
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 14:09:02 +0200 |
blanchet |
transform elim theorems before filtering "bool" and "prop" variables out;
|
file |
diff |
annotate
|
| Fri, 20 Aug 2010 13:39:47 +0200 |
blanchet |
more fiddling with Sledgehammer's "add:" option
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 19:34:11 +0200 |
blanchet |
generalize the "too general equality" code to handle facts like "x ~= A ==> x = B"
|
file |
diff |
annotate
|
| Thu, 19 Aug 2010 18:16:47 +0200 |
blanchet |
encode "fequal" reasoning rules in Metis problem, just as is done for Sledgehammer -- otherwise any proof that relies on "fequal" found by Sledgehammer can't be reconstructed
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 20:17:03 +0200 |
blanchet |
make sure that "add:" doesn't influence the relevance filter too much
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 19:57:12 +0200 |
blanchet |
tuning of relevance filter
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 18:01:54 +0200 |
blanchet |
minor cleanup
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 17:53:12 +0200 |
blanchet |
bound variables can be just as evil as schematic variables and lead to unsound proofs (e.g. "all_bool_eq")
|
file |
diff |
annotate
|
| Wed, 18 Aug 2010 16:39:05 +0200 |
blanchet |
fix the relevance filter so that it ignores If, Ex1, Ball, Bex
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 17:56:44 +0200 |
haftmann |
dropped dead code
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 14:08:30 +0200 |
blanchet |
prevent ATP thread for staying around for 1 minute if an exception occurred earlier;
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 14:00:32 +0200 |
blanchet |
adapt "too_general_equality" blacklisting to the new FOF context, where quantifiers are sometimes present
|
file |
diff |
annotate
|
| Mon, 09 Aug 2010 10:39:53 +0200 |
blanchet |
remove debugging output
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 22:57:36 +0200 |
blanchet |
handle division by zero gracefully (used to raise Unordered later on)
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 19:58:43 +0200 |
blanchet |
avoid "_def_raw" theorems
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 17:45:22 +0200 |
blanchet |
work around atomization failures
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 16:54:46 +0200 |
blanchet |
fiddle with the fudge factors, to get similar results as before
|
file |
diff |
annotate
|
| Thu, 29 Jul 2010 14:53:55 +0200 |
blanchet |
avoid "clause" and "cnf" terminology where it no longer makes sense
|
file |
diff |
annotate
|
| Tue, 27 Jul 2010 19:17:15 +0200 |
blanchet |
standardize "Author" tags
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:03:21 +0200 |
blanchet |
generate full first-order formulas (FOF) in Sledgehammer
|
file |
diff |
annotate
|
| Tue, 29 Jun 2010 10:25:53 +0200 |
blanchet |
move blacklisting completely out of the clausifier;
|
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:26:14 +0200 |
blanchet |
got rid of "respect_no_atp" option, which even I don't use
|
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:16:22 +0200 |
blanchet |
remove junk
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 15:08:03 +0200 |
blanchet |
further reduce dependencies on "sledgehammer_fact_filter.ML"
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 15:01:35 +0200 |
blanchet |
move "prepare_clauses" from "sledgehammer_fact_filter.ML" to "sledgehammer_hol_clause.ML";
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 12:15:24 +0200 |
blanchet |
eta-expand
|
file |
diff |
annotate
|
| Fri, 25 Jun 2010 12:08:48 +0200 |
blanchet |
improve the natural formula relevance filter code, so that it behaves more like the CNF one
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 18:22:15 +0200 |
blanchet |
a76ace919f1c wasn't quite right; second try
|
file |
diff |
annotate
|
| Thu, 24 Jun 2010 10:38:01 +0200 |
blanchet |
make sure that theorems passed using "add:" to Sledgehammer are not eliminated on heuristic grounds
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 18:43:50 +0200 |
blanchet |
improve the new "natural formula" fact filter
|
file |
diff |
annotate
|
| Wed, 23 Jun 2010 12:43:09 +0200 |
blanchet |
fix bug with "skolem_id" + sort facts for increased readability
|
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 18:47:45 +0200 |
blanchet |
missing "Unsynchronized" + make exception take a unit
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 18:31:49 +0200 |
blanchet |
added code to optionally perform fact filtering on the original (non-CNF) formulas
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 17:10:01 +0200 |
blanchet |
more cosmetics
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 17:07:39 +0200 |
blanchet |
cosmetics + prevent consideration of inlined Skolem terms in relevance filter
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 16:50:55 +0200 |
blanchet |
canonical argument order
|
file |
diff |
annotate
|
| Tue, 22 Jun 2010 16:40:36 +0200 |
blanchet |
leverage new data structure for handling "add:" and "del:"
|
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 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
|
| Mon, 07 Jun 2010 17:13:36 +0200 |
wenzelm |
made SML/NJ happy again;
|
file |
diff |
annotate
|
| Sat, 05 Jun 2010 21:30:40 +0200 |
blanchet |
renaming
|
file |
diff |
annotate
|
| Sat, 05 Jun 2010 16:39:23 +0200 |
blanchet |
show more respect for user-specified facts, even if they could lead to unsound proofs + don't throw away "unsound" theorems in "full_type" mode, since they are then sound
|
file |
diff |
annotate
|
| Sat, 05 Jun 2010 15:59:58 +0200 |
blanchet |
make Sledgehammer's "add:" and "del:" syntax work better in the presence of aliases;
|
file |
diff |
annotate
|
| Sat, 05 Jun 2010 15:07:50 +0200 |
blanchet |
totally bypass Sledgehammer's relevance filter when facts are given using the "(fact1 ... factn)" syntax;
|
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
|
| Mon, 17 May 2010 15:21:11 +0200 |
blanchet |
make sure chained facts don't pop up in the metis proof
|
file |
diff |
annotate
|
| Fri, 14 May 2010 16:15:10 +0200 |
blanchet |
renamed two Sledgehammer options
|
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
|
| Wed, 28 Apr 2010 18:11:11 +0200 |
blanchet |
make sure short theorem names are preferred to composite ones in Sledgehammer;
|
file |
diff |
annotate
|
| Tue, 27 Apr 2010 11:24:47 +0200 |
blanchet |
remove "higher_order" option from Sledgehammer -- the "smart" default is good enough
|
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
|
| Mon, 19 Apr 2010 16:33:20 +0200 |
blanchet |
make Sledgehammer's "add:" and "del:" syntax really work (I hope), by comparing CNF theorems with CNF theorems
|
file |
diff |
annotate
|
| Mon, 19 Apr 2010 10:45:08 +0200 |
blanchet |
rename Sledgehammer "theory_const" option to "theory_relevant", now that I understand better what it does
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 16:53:00 +0200 |
blanchet |
optimize relevance filter by doing a Table.fold directly rather than destroying the datastructure each time;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 16:08:43 +0200 |
blanchet |
reorganize Sledgehammer's relevance filter slightly
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 15:26:19 +0200 |
blanchet |
remove use of Polyhash;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 14:49:53 +0200 |
blanchet |
reintroduce efficient set structure to collect "no_atp" theorems
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 12:21:51 +0200 |
blanchet |
made "theory_const" a Sledgehammer option;
|
file |
diff |
annotate
|
| Mon, 29 Mar 2010 12:01:00 +0200 |
blanchet |
added "respect_no_atp" and "convergence" options to Sledgehammer;
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 14:51:36 +0100 |
blanchet |
revert debugging output that shouldn't have been submitted in the first place
|
file |
diff |
annotate
|
| Wed, 24 Mar 2010 12:30:33 +0100 |
blanchet |
honor the newly introduced Sledgehammer parameters and fixed the parsing;
|
file |
diff |
annotate
|
| Tue, 23 Mar 2010 11:39:21 +0100 |
blanchet |
added options to Sledgehammer;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 13:02:18 +0100 |
blanchet |
more Sledgehammer refactoring
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
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
|