src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
Wed, 22 Sep 2021 12:25:09 +0200 desharna enabled FOOL for Vampire in Sledgehammer
Wed, 22 Sep 2021 10:46:42 +0200 desharna used Vampire 4.5.1 in Sledgehammer
Wed, 15 Sep 2021 16:02:04 +0200 wenzelm clarified name and options for old vampire-4.2.2;
Fri, 27 Aug 2021 14:29:02 +0200 blanchet handle Zipperposition's ResourceOut gracefully
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
Wed, 04 Aug 2021 08:23:12 +0200 desharna added dummy_fof prover to Sledgehammer
Tue, 03 Aug 2021 09:22:38 +0200 desharna added dummy_thf prover to Sledgehammer
Mon, 19 Jul 2021 14:47:52 +0200 blanchet tuned E's lambda encoding
Mon, 19 Jul 2021 10:38:14 +0200 blanchet use Vampire's clausifier with iProver, now that E's is no longer supported
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
Tue, 13 Jul 2021 10:57:14 +0200 blanchet wait for E 2.7 before using 'ite' in HO mode
Tue, 13 Jul 2021 10:57:14 +0200 blanchet added alternative E binary name
Mon, 12 Jul 2021 16:30:15 +0200 blanchet adjusted E setup to avoid generating FOOL with 2.5 (where 'ite' is missing)
Thu, 17 Jun 2021 12:57:22 +0200 desharna added support for TFX's and THF's $ite to Sledgehammer
Mon, 12 Apr 2021 22:16:31 +0200 wenzelm clarified signature: more structured arguments, notably for remote provers;
Sun, 14 Mar 2021 21:41:28 +0100 wenzelm proper shell quote;
Sun, 14 Mar 2021 21:02:34 +0100 wenzelm removed spurious references to perl / libwww-perl;
Sun, 14 Mar 2021 20:29:26 +0100 wenzelm invoke remote ATP via SystemOnTPTP.run_systems from Isabelle/Scala (without perl);
Sun, 14 Mar 2021 16:50:11 +0100 wenzelm clarified signature: more explicit types;
Sat, 13 Mar 2021 15:14:46 +0100 wenzelm use SystemOnTPTP.list_systems from Isabelle/Scala, with dynamic URL option and more elementary error messages;
Thu, 04 Mar 2021 11:06:39 +0100 desharna tuned best_slices in atp_config
Thu, 04 Mar 2021 10:10:44 +0100 desharna tuned exec field in atp_config
Tue, 23 Feb 2021 12:20:50 +0100 desharna proper usage of hypotheses for zipperposition's TPTP generation
Tue, 23 Feb 2021 10:13:09 +0100 desharna merged
Fri, 12 Feb 2021 11:18:12 +0100 desharna proper prover capabilities for zipperposition
Mon, 22 Feb 2021 15:24:04 +0100 wenzelm clarified signature: always trim_line of Process_Result.out/err, uniformly in ML and Scala;
Wed, 16 Dec 2020 13:39:49 +0100 desharna enabled FOOL for E
Thu, 26 Nov 2020 18:45:19 +0100 desharna proper parsing of type encoding;
Thu, 19 Nov 2020 15:11:37 +0100 desharna reintroduced and renamed THF_Predicate_Free deleted by c7e2a9bdc585
Thu, 19 Nov 2020 14:46:49 +0100 desharna repaired thf output broken by c7e2a9bdc585
Thu, 05 Nov 2020 18:14:02 +0100 desharna Added support for TFX to Sledgehammer
Thu, 08 Oct 2020 17:55:17 +0200 blanchet removed support for obsolete prover SNARK and underperforming prover E-Par
Thu, 08 Oct 2020 17:46:03 +0200 blanchet removed obsolete unmaintained experimental prover Pirate
Thu, 08 Oct 2020 17:02:56 +0200 desharna tune filename
less more (0) tip