Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
Tue, 07 Jan 2025 20:47:42 +0100 wenzelm tuned: more direct string comparison (see also 6e25f82056ad, where the explanation was actually wrong: about fast_string_ord instead of string_ord); file | diff | annotate
Sun, 05 Jan 2025 15:18:30 +0100 wenzelm tuned (NB: string_ord is required here for its precedence on length); file | diff | annotate
Wed, 06 Mar 2024 09:26:40 +0100 desharna removed unused variable file | diff | annotate
Wed, 06 Mar 2024 09:25:34 +0100 desharna added virtual, greedy portfolio for E 3.0 file | diff | annotate
Fri, 20 Oct 2023 12:25:35 +0200 desharna proper slice duration (i.e., 5 s) for new Vampire portfolio following 5a14f2cc1ea0 file | diff | annotate
Wed, 18 Oct 2023 10:41:12 +0200 desharna added new portfolio for Vampire 4.8 file | diff | annotate
Fri, 25 Aug 2023 11:31:24 +0200 blanchet avoid using FOOL syntax with older Vampire versions because of soundness bug visible by passing 'Abs_unit_cases Rep_unit Rep_unit_cases' as the facts to Sledgehammer file | diff | annotate
Wed, 01 Mar 2023 08:00:51 +0100 blanchet there won't be an E version 2.7 file | diff | annotate
Wed, 01 Mar 2023 08:00:51 +0100 blanchet adopt terminology suggested by Larry Paulson file | diff | annotate
Wed, 01 Mar 2023 08:00:51 +0100 blanchet renamed new Sledgehammer option 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 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
Sat, 17 Sep 2022 16:50:39 +0200 wenzelm proper file headers; file | diff | annotate
Wed, 17 Aug 2022 15:09:53 +0200 blanchet tweak Sledgehammer's slicing mechanism -- updated Zipperposition's slices and make them half as long as other provers' to pack more of them in 30 s file | diff | annotate
Tue, 02 Aug 2022 13:23:57 +0200 blanchet changed the order of Zipperposition slices in Sledgehammer file | diff | annotate
Fri, 27 May 2022 13:46:40 +0200 desharna excluded dummy ATPs from Sledgehammer's default provers file | diff | annotate
Wed, 13 Apr 2022 16:53:46 +0200 blanchet pass new option only to new version of E file | diff | annotate
Fri, 08 Apr 2022 17:17:21 +0200 blanchet enable an E option suggested by Petar Vukmirovic file | diff | annotate
Thu, 31 Mar 2022 18:14:11 +0200 blanchet further tweaked E's setup file | diff | annotate
Thu, 31 Mar 2022 15:26:18 +0200 blanchet tweaked E setup file | diff | annotate
Fri, 25 Mar 2022 13:52:23 +0100 blanchet further modernized E setup 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, 02 Feb 2022 13:34:52 +0100 blanchet enable induction in one of Zipperposition's slices file | diff | annotate
Tue, 01 Feb 2022 12:49:14 +0100 blanchet don't pass --auto-schedule to E indiscriminately -- use it instead of 'auto' in one slice file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet removed experimental prover z3_tptp file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet run all installed provers by default file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet further work on new Sledgehammer slicing file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet crude implementation of centralized slicing file | diff | annotate
Mon, 31 Jan 2022 16:09:23 +0100 blanchet removed obscure E option 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
Fri, 21 Jan 2022 21:09:55 +0100 desharna proper fact filter for dummy ATPs file | diff | annotate
Wed, 05 Jan 2022 10:56:41 +0100 desharna removed $ite from E 2.6 in THF format file | diff | annotate
Sat, 18 Dec 2021 23:17:08 +0100 desharna used TH1 for Leo-III in sledgehammer file | diff | annotate
Fri, 19 Nov 2021 11:04:53 +0100 desharna proper polymorphism for TH1 format in Sledgehammer file | diff | annotate
Fri, 19 Nov 2021 10:53:22 +0100 desharna refactored $ite and $let configuration and added dummy_thf_reduced prover file | diff | annotate
Fri, 12 Nov 2021 00:10:16 +0100 desharna separated FOOL from $ite/$let in TPTP output file | diff | annotate
Wed, 20 Oct 2021 18:13:17 +0200 wenzelm discontinued obsolete "val extend = I" for data slots; file | diff | annotate
Thu, 14 Oct 2021 16:56:02 +0200 desharna tuned Vampire configuration to use TFX in Sledgehammer file | diff | annotate
Mon, 04 Oct 2021 10:17:11 +0200 desharna tuned zipperposition config in sledgehammer file | diff | annotate
Wed, 29 Sep 2021 16:47:53 +0200 desharna tuned Zipperposition slides in sledgehammer file | diff | annotate
Tue, 28 Sep 2021 12:35:43 +0200 desharna updated to Zipperposition 2.1 file | diff | annotate
Wed, 22 Sep 2021 12:41:40 +0200 desharna removed checks for non-commercial usage of Vampire as it is now under BSD licence file | diff | annotate
Wed, 22 Sep 2021 12:25:09 +0200 desharna enabled FOOL for Vampire in Sledgehammer file | diff | annotate
Wed, 22 Sep 2021 10:46:42 +0200 desharna used Vampire 4.5.1 in Sledgehammer file | diff | annotate
Wed, 15 Sep 2021 16:02:04 +0200 wenzelm clarified name and options for old vampire-4.2.2; file | diff | annotate
Fri, 27 Aug 2021 14:29:02 +0200 blanchet handle Zipperposition's ResourceOut gracefully file | diff | annotate
Fri, 27 Aug 2021 14:28:56 +0200 blanchet disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax file | diff | annotate
Wed, 04 Aug 2021 08:23:12 +0200 desharna added dummy_fof prover to Sledgehammer file | diff | annotate
Tue, 03 Aug 2021 09:22:38 +0200 desharna added dummy_thf prover to Sledgehammer file | diff | annotate
Mon, 19 Jul 2021 14:47:52 +0200 blanchet tuned E's lambda encoding file | diff | annotate
Mon, 19 Jul 2021 10:38:14 +0200 blanchet use Vampire's clausifier with iProver, now that E's is no longer supported file | diff | annotate
Fri, 16 Jul 2021 15:27:55 +0200 blanchet get rid of remote_vampire since it's hard, if possible at all, to follow Vampire's online options file | diff | annotate
Tue, 13 Jul 2021 10:57:14 +0200 blanchet wait for E 2.7 before using 'ite' in HO mode file | diff | annotate
Tue, 13 Jul 2021 10:57:14 +0200 blanchet added alternative E binary name file | diff | annotate
Mon, 12 Jul 2021 16:30:15 +0200 blanchet adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing) file | diff | annotate
less more (0) -60 tip
isabelle