# HG changeset patch # User blanchet # Date 1510064201 -3600 # Node ID 41f1f8c4259b8f9b0ac8dfa1d16b8e54caf36bb3 # Parent c32254ab1901cf6023a9d51acb608aa88ce56738 integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch) diff -r c32254ab1901 -r 41f1f8c4259b src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Tue Nov 07 15:16:40 2017 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Tue Nov 07 15:16:41 2017 +0100 @@ -107,7 +107,7 @@ The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver \cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II -\cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS +\cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002}, Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}. The ATPs are run either locally or remotely via the System\-On\-TPTP web service @@ -154,9 +154,9 @@ Sledgehammer is part of Isabelle, so you do not need to install it. However, it relies on third-party automatic provers (ATPs and SMT solvers). -Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, Vampire, and +Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF, -iProver, iProver-Eq, LEO-II, Satallax, SNARK, Vampire, and Waldmeister are +iProver, iProver-Eq, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers CVC3, CVC4, veriT, and Z3 can be run locally. @@ -184,26 +184,26 @@ in it. -\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, or +\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, or Satallax manually, or found a Vampire executable somewhere (e.g., \url{http://www.vprover.org/}), set the environment variable \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME}, -\texttt{SATALLAX\_HOME}, or +\texttt{LEO3\_HOME}, \texttt{SATALLAX\_HOME}, or \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL}, \texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}), -\texttt{leo}, \texttt{satallax}, or \texttt{vampire} executable; +\texttt{leo}, \texttt{leo3}, \texttt{satallax}, or \texttt{vampire} executable; for Alt-Ergo, set the environment variable \texttt{WHY3\_HOME} to the directory that contains the \texttt{why3} executable. Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0, -LEO-II 1.3.4, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.% +LEO-II 1.3.4, Leo-III 1.1, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.% \footnote{Following the rewrite of Vampire, the counter for version numbers was reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more recent than 9.0 or 11.5.}% Since the ATPs' output formats are neither documented nor stable, other versions might not work well with Sledgehammer. Ideally, you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION}, -\texttt{SATALLAX\_VERSION}, or +\texttt{LEO3\_VERSION}, \texttt{SATALLAX\_VERSION}, or \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0''). Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment @@ -787,6 +787,13 @@ the environment variable \texttt{LEO2\_HOME} to the directory that contains the \texttt{leo} executable. Sledgehammer requires version 1.3.4 or above. +\item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic +higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph +Benzm\"uller et al.\ \cite{leo3}, +with support for the TPTP typed higher-order syntax (THF0). To use Leo-III, set +the environment variable \texttt{LEO3\_HOME} to the directory that contains the +\texttt{leo3} executable. Sledgehammer requires version 1.1 or above. + \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the @@ -865,6 +872,9 @@ \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. +\item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III +runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}. + \item[\labelitemi] \textbf{\textit{remote\_pirate}:} Pirate is a highly experimental first-order resolution prover developed by Daniel Wand. The remote version of Pirate run on a private server he generously set up. diff -r c32254ab1901 -r 41f1f8c4259b src/Doc/manual.bib --- a/src/Doc/manual.bib Tue Nov 07 15:16:40 2017 +0100 +++ b/src/Doc/manual.bib Tue Nov 07 15:16:41 2017 +0100 @@ -1831,11 +1831,19 @@ crossref = {tphols96}, pages = {381-397}} -@inproceedings{snark, - author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood}, - title = {Deductive composition of astronomical software from subroutine libraries}, - pages = "341--355", - crossref = {cade12}} +@inproceedings{leo3, + Author = {Alexander Steen and Max Wisniewski and Christoph + Benzm{\"u}ller}, + Booktitle = {Mathematical Software -- ICMS 2016}, + Editor = {G.-M. Greuel and T. Koch and P. Paule and + A. Sommese}, + Publisher = {Springer}, + Series = {LNCS}, + Title = {Agent-Based {HOL} Reasoning}, + Volume = 9725, + Year = 2016, + Pages = {75-81} +} @incollection{sternagel-thiemann-2015, title = "Deriving Class Instances for Datatypes", @@ -1846,6 +1854,12 @@ month = "March", year = 2015} +@inproceedings{snark, + author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood}, + title = {Deductive composition of astronomical software from subroutine libraries}, + pages = "341--355", + crossref = {cade12}} + @book{suppes72, author = {Patrick Suppes}, title = {Axiomatic Set Theory}, diff -r c32254ab1901 -r 41f1f8c4259b src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Tue Nov 07 15:16:40 2017 +0100 +++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Nov 07 15:16:41 2017 +0100 @@ -57,6 +57,7 @@ val iproverN : string val iprover_eqN : string val leo2N : string + val leo3N : string val pirateN : string val satallaxN : string val snarkN : string @@ -126,6 +127,7 @@ val iproverN = "iprover" val iprover_eqN = "iprover_eq" val leo2N = "leo2" +val leo3N = "leo3" val pirateN = "pirate" val satallaxN = "satallax" val snarkN = "snark" @@ -681,7 +683,7 @@ >> map (core_inference z3_tptp_core_rule)) x fun parse_line local_name problem = - if local_name = leo2N then parse_tstp_thf0_line problem + if local_name = leo2N orelse local_name = leo3N then parse_tstp_thf0_line problem else if local_name = spassN then parse_spass_line else if local_name = pirateN then parse_pirate_line else if local_name = z3_tptpN then parse_z3_tptp_core_line diff -r c32254ab1901 -r 41f1f8c4259b src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Nov 07 15:16:40 2017 +0100 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Nov 07 15:16:41 2017 +0100 @@ -416,6 +416,29 @@ val leo2 = (leo2N, fn () => leo2_config) +(* Leo-III *) + +(* include choice? Disabled now since its disabled for satallax as well. *) +val leo3_thf1 = THF (Polymorphic, THF_Without_Choice) + +val leo3_config : atp_config = + {exec = K (["LEO3_HOME"], ["leo3"]), + arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ => + file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \ + \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^ + (if full_proofs then "--nleq --naeq " else ""), + proof_delims = tstp_proof_delims, + known_failures = known_szs_status_failures, + prem_role = Hypothesis, + best_slices = + (* FUDGE *) + K [(1.0, (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), ""))], + best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), + best_max_new_mono_instances = default_max_new_mono_instances} + +val leo3 = (leo3N, fn () => leo3_config) + + (* Satallax *) (* Choice is disabled until there is proper reconstruction for it. *) @@ -431,7 +454,7 @@ prem_role = Hypothesis, best_slices = (* FUDGE *) - K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))], + K [(1.0, (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))], best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *), best_max_new_mono_instances = default_max_new_mono_instances} @@ -713,9 +736,12 @@ val remote_leo2 = remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"] (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *)) +val remote_leo3 = + remotify_atp leo3 "Leo-III" ["1.1"] + (K (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_satallax = remotify_atp satallax "Satallax" ["2.7", "2.3", "2"] - (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) + (K (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *)) val remote_vampire = remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"] (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *)) @@ -766,10 +792,10 @@ end val atps = - [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire, + [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine, - remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, - remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new] + remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_satallax, + remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new] val _ = Theory.setup (fold add_atp atps)