Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
make "prepare_atp_problem" more robust w.r.t. choice of type system
|
file |
diff |
annotate
|
Tue, 31 May 2011 16:38:36 +0200 |
blanchet |
don't preprocess twice
|
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 |
first step in sharing more code between ATP and Metis translation
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
don't slice if there are too few facts
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
automatically minimize with Metis when this can be done within a few seconds
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
minimize with Metis if possible
|
file |
diff |
annotate
|
Mon, 30 May 2011 17:00:38 +0200 |
blanchet |
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
|
file |
diff |
annotate
|
Sun, 29 May 2011 19:40:56 +0200 |
blanchet |
always check plain "metis" even if the ATP proof seems to require "metisFT" -- maybe the proof is needlessly complicated
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
cleanup proof text generation code
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
try both "metis" and (on failure) "metisFT" in replay
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
show time taken for reconstruction
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
more concise output
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
handle non-auto try case of Sledgehammer better
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:08 +0200 |
blanchet |
renamed "metis_timeout" to "preplay_timeout" and continued implementation
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
added syntax for specifying Metis timeout (currently used only by SMT solvers)
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
make output more concise
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
merge timeout messages from several ATPs into one message to avoid clutter
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fix soundness bug in Sledgehammer: distinguish params in goals from fixed variables in context
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
fully support all type system encodings in typed formats (TFF, THF)
|
file |
diff |
annotate
|
Fri, 27 May 2011 10:30:07 +0200 |
blanchet |
towards supporting non-simply-typed encodings for TFF and THF (for orthogonality and experiments)
|
file |
diff |
annotate
|
Tue, 24 May 2011 17:04:35 +0200 |
blanchet |
respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")
|
file |
diff |
annotate
|
Tue, 24 May 2011 10:01:03 +0200 |
blanchet |
more work on parsing LEO-II proofs and extracting uses of extensionality
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
slightly gracefuller handling of LEO-II and Satallax output
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
identify HOL functions with THF functions
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
started adding support for THF output (but no lambdas)
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
filter Waldmeister facts better -- and don't encode type classes as predicates, since it doesn't like conditional equations
|
file |
diff |
annotate
|
Tue, 24 May 2011 00:01:33 +0200 |
blanchet |
tuning -- the "appropriate" terminology is inspired from TPTP
|
file |
diff |
annotate
|
Sun, 22 May 2011 14:51:42 +0200 |
blanchet |
improved Waldmeister support -- even run it by default on unit equational goals
|
file |
diff |
annotate
|
Sun, 22 May 2011 14:51:41 +0200 |
blanchet |
fish out axioms in Waldmeister output
|
file |
diff |
annotate
|
Sun, 22 May 2011 14:51:01 +0200 |
blanchet |
added support for remote Waldmeister
|
file |
diff |
annotate
|
Sun, 22 May 2011 14:49:35 +0200 |
blanchet |
reorganized ATP formats a little bit
|
file |
diff |
annotate
|
Fri, 20 May 2011 12:47:59 +0200 |
blanchet |
make sure the Vampire incomplete proof detection code kicks in
|
file |
diff |
annotate
|
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, 19 May 2011 10:24:13 +0200 |
blanchet |
tweaked ATP type systems further based on Judgment Day
|
file |
diff |
annotate
|
Thu, 19 May 2011 10:24:13 +0200 |
blanchet |
reintroduce TFF workaround for limitations of actual TFF implementations (ToFoF, SNARK)
|
file |
diff |
annotate
|
Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
renamed thin to light, fat to heavy
|
file |
diff |
annotate
|
Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
run blacklist algorithm only if slicing is on
|
file |
diff |
annotate
|
Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
renamed "shallow" to "thin" and make it the default
|
file |
diff |
annotate
|
Tue, 17 May 2011 15:11:36 +0200 |
blanchet |
added syntax for "shallow" encodings
|
file |
diff |
annotate
|
Fri, 13 May 2011 10:10:43 +0200 |
blanchet |
tuned comment
|
file |
diff |
annotate
|
Fri, 13 May 2011 10:10:43 +0200 |
blanchet |
fixed off-by-one bug
|
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 |
further lower penalty associated with existentials in Sledgehammer's relevance filter, so that "exhaust" facts are picked up
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
renamed "max_mono_instances" to "max_new_mono_instances" and changed its semantics accordingly
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
remove unused parameter
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
reduced penalty associated with existential quantifiers
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
fine-tuned the relevance filter, so that equations of the form "c = (%x. _)" and constants occurring in chained facts are not unduely penalized
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
improve detection of quantifications over dangerous types by leveraging "is_type_surely_finite" predicate and added "prop" to the list of surely finite types
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:19 +0200 |
blanchet |
tune whitespace
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
added "max_mono_instances" option to Sledgehammer and renamed old "monomorphize_limit" option
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
allow each slice to have its own type system
|
file |
diff |
annotate
|
Thu, 12 May 2011 15:29:18 +0200 |
blanchet |
renamed type systems for more consistency
|
file |
diff |
annotate
|
Fri, 06 May 2011 13:34:59 +0200 |
blanchet |
allow each prover to specify its own formula kind for symbols occurring in the conjecture
|
file |
diff |
annotate
|
Thu, 05 May 2011 12:40:48 +0200 |
blanchet |
no lies in debug output (e.g. "slice 2 of 1")
|
file |
diff |
annotate
|
Wed, 04 May 2011 22:56:33 +0200 |
blanchet |
renamed "many_typed" to "simple" (as in simple types)
|
file |
diff |
annotate
|
Wed, 04 May 2011 22:47:13 +0200 |
blanchet |
added type homogenization, whereby all (isomorphic) infinite types are mapped to the same type (to reduce the number of different predicates/TFF-types)
|
file |
diff |
annotate
|
Tue, 03 May 2011 21:46:49 +0200 |
blanchet |
fixed per-ATP dangerous axiom detection -- embarrassing bugs introduced in change a7a30721767a
|
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
|