| Fri, 10 Mar 2023 15:27:18 +0100 |
blanchet |
use simplifier to classify the missing assumptions in Sledgehammer's abduction mechanism
|
file |
diff |
annotate
|
| Fri, 03 Mar 2023 10:30:10 +0100 |
blanchet |
got rid of 'important message' mechanism in SystemOnTPTP (which is less used nowadays)
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
tweaked Sledgehammer interaction
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
reverted 0506c3273814 -- the message is still useful
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
tweaked abduction in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 01 Mar 2023 08:00:51 +0100 |
blanchet |
implemented ad hoc abduction in Sledgehammer with E
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 17:01:42 +0100 |
blanchet |
removed rarely used error in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 15 Feb 2023 10:56:23 +0100 |
blanchet |
added refute mode to Sledgehammer to find 'counterexamples'
|
file |
diff |
annotate
|
| Mon, 17 Oct 2022 13:04:00 +0200 |
blanchet |
generate some metainformation not only for SPASS but also for Zipperposition, for experimentation
|
file |
diff |
annotate
|
| Tue, 16 Aug 2022 17:24:58 +0200 |
blanchet |
revived 'try0' and 'smart' Isar proofs in Sledgehammer
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
cleaned up obsolete E setup and a bit of SPASS
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
second and last step in making time slicing more flexible in Sledgehammer: try to honor desired slice size
|
file |
diff |
annotate
|
| Fri, 25 Mar 2022 13:52:23 +0100 |
blanchet |
first step in making time slicing more flexible in Sledgehammer: label slices with 'slice size'
|
file |
diff |
annotate
|
| Wed, 09 Feb 2022 14:52:05 +0100 |
desharna |
uniformized fact selection for ATP and SMT in Sledgehammer
|
file |
diff |
annotate
|
| Wed, 09 Feb 2022 13:02:59 +0100 |
desharna |
used max_facts and fact_filter from slice for both ATP and SMT in sledgehammer
|
file |
diff |
annotate
|
| Mon, 07 Feb 2022 16:59:37 +0100 |
blanchet |
more robust TSTP proof parsing
|
file |
diff |
annotate
|
| Mon, 07 Feb 2022 15:26:22 +0100 |
blanchet |
added possibility of extra options to SMT slices
|
file |
diff |
annotate
|
| Wed, 02 Feb 2022 13:43:48 +0100 |
blanchet |
more precise slicing computation and output when not enough lemmas are available (e.g. with the 'only' syntax 'sledgehammer (lem1 lem2 lem3)')
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
update slice options centrally
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalize slicing format
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
thread slices through
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
simplified 'best_slice' data structure and made minor changes to slices
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
rationalized output for forthcoming slicing model
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
disable slicing within ATP module (in preparation for refactoring)
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
disable slicing within SMT (in preparation for factoring it out)
|
file |
diff |
annotate
|
| Mon, 31 Jan 2022 16:09:23 +0100 |
blanchet |
generalized the 'slice' option towards more flexible slicing
|
file |
diff |
annotate
|
| Fri, 21 Jan 2022 21:10:34 +0100 |
desharna |
added spying to Sledgehammer
|
file |
diff |
annotate
|
| Tue, 11 Jan 2022 22:07:04 +0100 |
desharna |
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
|
file |
diff |
annotate
|
| Fri, 10 Dec 2021 16:46:29 +0100 |
desharna |
tuned sledgehammer to use map_index
|
file |
diff |
annotate
|
| Wed, 17 Nov 2021 21:36:13 +0100 |
desharna |
tuned TPTP file names generated by Sledgehammer
|
file |
diff |
annotate
|
| Mon, 04 Oct 2021 10:16:42 +0200 |
desharna |
considered slices overhead in sledgehammer
|
file |
diff |
annotate
|
| Wed, 29 Sep 2021 16:48:23 +0200 |
desharna |
tuned atp_prover sliding
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 22:08:51 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2021 14:18:46 +0200 |
wenzelm |
provide bash_process server for Isabelle/ML and other external programs;
|
file |
diff |
annotate
|
| Sat, 07 Aug 2021 22:23:37 +0200 |
wenzelm |
clarified signature: more options for bash_process;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 08:42:36 +0200 |
desharna |
added opaque_combs and renamed hide_lams to opaque_lifting
|
file |
diff |
annotate
|
| Sun, 25 Apr 2021 22:33:15 +0200 |
wenzelm |
avoid "exec" to change the winpid;
|
file |
diff |
annotate
|
| Mon, 12 Apr 2021 22:16:31 +0200 |
wenzelm |
clarified signature: more structured arguments, notably for remote provers;
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 20:29:26 +0100 |
wenzelm |
invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
|
file |
diff |
annotate
|
| Sun, 14 Mar 2021 16:50:11 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2021 19:29:45 +0100 |
wenzelm |
more direct elapsed run_time via bash_process wrapper (via Scala and C);
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 10:10:44 +0100 |
desharna |
tuned exec field in atp_config
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 16:07:41 +0100 |
desharna |
Added smt (verit) to Sledgehammer's proof preplay.
|
file |
diff |
annotate
|
| Tue, 27 Oct 2020 22:34:37 +0100 |
wenzelm |
clarified signature: overloaded "+" for Path.append;
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:46:03 +0200 |
blanchet |
removed obsolete unmaintained experimental prover Pirate
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 17:02:56 +0200 |
desharna |
tune filename
|
file |
diff |
annotate
|
| Thu, 08 Oct 2020 16:36:00 +0200 |
desharna |
drop obsolete ad hoc support for Satallax isar proof reconstruction
|
file |
diff |
annotate
|
| Wed, 10 Jun 2020 15:55:41 +0200 |
blanchet |
simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)
|
file |
diff |
annotate
|
| Fri, 25 Oct 2019 14:14:56 +0200 |
blanchet |
removed experimental encoding for Waldmeister
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
killed final stops in Sledgehammer and friends
|
file |
diff |
annotate
|
| Sat, 02 Apr 2016 23:29:05 +0200 |
wenzelm |
prefer infix operations;
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
early warning when Sledgehammer finds a proof
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
refined experimental option of Sledgehammer
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 21:09:28 +0100 |
wenzelm |
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 17:01:45 +0100 |
wenzelm |
tuned signature -- clarified modules;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:41:14 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 20:02:51 +0100 |
blanchet |
cleaner generation of metainformation in DFG format and TPTP theory exporter for Sledgehammer
|
file |
diff |
annotate
|