integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
authorblanchet
Tue Nov 07 15:16:41 2017 +0100 (7 months ago)
changeset 6702141f1f8c4259b
parent 67020 c32254ab1901
child 67022 49309fe530fd
integrated Leo-III in Sledgehammer (thanks to Alexander Steen for the patch)
src/Doc/Sledgehammer/document/root.tex
src/Doc/manual.bib
src/HOL/Tools/ATP/atp_proof.ML
src/HOL/Tools/ATP/atp_systems.ML
     1.1 --- a/src/Doc/Sledgehammer/document/root.tex	Tue Nov 07 15:16:40 2017 +0100
     1.2 +++ b/src/Doc/Sledgehammer/document/root.tex	Tue Nov 07 15:16:41 2017 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4  The supported ATPs are AgsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E
     1.5  \cite{schulz-2002}, E-SInE \cite{sine}, E-ToFoF \cite{tofof}, iProver
     1.6  \cite{korovin-2009}, iProver-Eq \cite{korovin-sticksel-2010}, LEO-II
     1.7 -\cite{leo2}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
     1.8 +\cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, SNARK \cite{snark}, SPASS
     1.9  \cite{weidenbach-et-al-2009}, Vampire \cite{riazanov-voronkov-2002},
    1.10  Waldmeister \cite{waldmeister}, and Zipperposition \cite{cruanes-2014}.
    1.11  The ATPs are run either locally or remotely via the System\-On\-TPTP web service
    1.12 @@ -154,9 +154,9 @@
    1.13  Sledgehammer is part of Isabelle, so you do not need to install it. However, it
    1.14  relies on third-party automatic provers (ATPs and SMT solvers).
    1.15  
    1.16 -Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Satallax, SPASS, Vampire, and
    1.17 +Among the ATPs, AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, Satallax, SPASS, Vampire, and
    1.18  Zipperposition can be run locally; in addition, AgsyHOL, E, E-SInE, E-ToFoF,
    1.19 -iProver, iProver-Eq, LEO-II, Satallax, SNARK, Vampire, and Waldmeister are
    1.20 +iProver, iProver-Eq, LEO-II, Leo-III, Satallax, SNARK, Vampire, and Waldmeister are
    1.21  available remotely via System\-On\-TPTP \cite{sutcliffe-2000}. The SMT solvers
    1.22  CVC3, CVC4, veriT, and Z3 can be run locally.
    1.23  
    1.24 @@ -184,26 +184,26 @@
    1.25  
    1.26  in it.
    1.27  
    1.28 -\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, or
    1.29 +\item[\labelitemi] If you prefer to build AgsyHOL, Alt-Ergo, E, LEO-II, Leo-III, or
    1.30  Satallax manually, or found a Vampire executable somewhere (e.g.,
    1.31  \url{http://www.vprover.org/}), set the environment variable
    1.32  \texttt{AGSYHOL\_HOME}, \texttt{E\_HOME}, \texttt{LEO2\_HOME},
    1.33 -\texttt{SATALLAX\_HOME}, or
    1.34 +\texttt{LEO3\_HOME}, \texttt{SATALLAX\_HOME}, or
    1.35  \texttt{VAMPIRE\_HOME} to the directory that contains the \texttt{agsyHOL},
    1.36  \texttt{eprover} (and/or \texttt{eproof} or \texttt{eproof\_ram}),
    1.37 -\texttt{leo}, \texttt{satallax}, or \texttt{vampire} executable;
    1.38 +\texttt{leo}, \texttt{leo3}, \texttt{satallax}, or \texttt{vampire} executable;
    1.39  for Alt-Ergo, set the
    1.40  environment variable \texttt{WHY3\_HOME} to the directory that contains the
    1.41  \texttt{why3} executable.
    1.42  Sledgehammer has been tested with AgsyHOL 1.0, Alt-Ergo 0.95.2, E 1.6 to 2.0,
    1.43 -LEO-II 1.3.4, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.%
    1.44 +LEO-II 1.3.4, Leo-III 1.1, Satallax 2.2 to 2.7, and Vampire 0.6 to 4.0.%
    1.45  \footnote{Following the rewrite of Vampire, the counter for version numbers was
    1.46  reset to 0; hence the (new) Vampire versions 0.6, 1.0, 1.8, 2.6, and 3.0 are more
    1.47  recent than 9.0 or 11.5.}%
    1.48  Since the ATPs' output formats are neither documented nor stable, other
    1.49  versions might not work well with Sledgehammer. Ideally,
    1.50  you should also set \texttt{E\_VERSION}, \texttt{LEO2\_VERSION},
    1.51 -\texttt{SATALLAX\_VERSION}, or
    1.52 +\texttt{LEO3\_VERSION}, \texttt{SATALLAX\_VERSION}, or
    1.53  \texttt{VAMPIRE\_VERSION} to the prover's version number (e.g., ``4.0'').
    1.54  
    1.55  Similarly, if you want to install CVC3, CVC4, veriT, or Z3, set the environment
    1.56 @@ -787,6 +787,13 @@
    1.57  the environment variable \texttt{LEO2\_HOME} to the directory that contains the
    1.58  \texttt{leo} executable. Sledgehammer requires version 1.3.4 or above.
    1.59  
    1.60 +\item[\labelitemi] \textbf{\textit{leo3}:} Leo-III is an automatic
    1.61 +higher-order prover developed by Alexander Steen, Max Wisniewski, Christoph
    1.62 +Benzm\"uller et al.\ \cite{leo3},
    1.63 +with support for the TPTP typed higher-order syntax (THF0). To use Leo-III, set
    1.64 +the environment variable \texttt{LEO3\_HOME} to the directory that contains the
    1.65 +\texttt{leo3} executable. Sledgehammer requires version 1.1 or above.
    1.66 +
    1.67  \item[\labelitemi] \textbf{\textit{satallax}:} Satallax is an automatic
    1.68  higher-order prover developed by Chad Brown et al.\ \cite{satallax}, with
    1.69  support for the TPTP typed higher-order syntax (THF0). To use Satallax, set the
    1.70 @@ -865,6 +872,9 @@
    1.71  \item[\labelitemi] \textbf{\textit{remote\_leo2}:} The remote version of LEO-II
    1.72  runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
    1.73  
    1.74 +\item[\labelitemi] \textbf{\textit{remote\_leo3}:} The remote version of Leo-III
    1.75 +runs on Geoff Sutcliffe's Miami servers \cite{sutcliffe-2000}.
    1.76 +
    1.77  \item[\labelitemi] \textbf{\textit{remote\_pirate}:} Pirate is a
    1.78  highly experimental first-order resolution prover developed by Daniel Wand.
    1.79  The remote version of Pirate run on a private server he generously set up.
     2.1 --- a/src/Doc/manual.bib	Tue Nov 07 15:16:40 2017 +0100
     2.2 +++ b/src/Doc/manual.bib	Tue Nov 07 15:16:41 2017 +0100
     2.3 @@ -1831,11 +1831,19 @@
     2.4    crossref  = {tphols96},
     2.5    pages		= {381-397}}
     2.6  
     2.7 -@inproceedings{snark,
     2.8 -  author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood},
     2.9 -  title = {Deductive composition of astronomical software from subroutine libraries},
    2.10 -  pages = "341--355",
    2.11 -  crossref = {cade12}}
    2.12 +@inproceedings{leo3,
    2.13 +  Author =	 {Alexander Steen and Max Wisniewski and Christoph
    2.14 +                  Benzm{\"u}ller},
    2.15 +  Booktitle =	 {Mathematical Software -- ICMS 2016},
    2.16 +  Editor =	 {G.-M. Greuel and T. Koch and P. Paule and
    2.17 +                  A. Sommese},
    2.18 +  Publisher =	 {Springer},
    2.19 +  Series =	 {LNCS},
    2.20 +  Title =	 {Agent-Based {HOL} Reasoning},
    2.21 +  Volume =	 9725,
    2.22 +  Year =	 2016,
    2.23 +  Pages =	 {75-81}
    2.24 +}
    2.25  
    2.26  @incollection{sternagel-thiemann-2015,
    2.27    title = "Deriving Class Instances for Datatypes",
    2.28 @@ -1846,6 +1854,12 @@
    2.29    month = "March",
    2.30    year = 2015}
    2.31  
    2.32 +@inproceedings{snark,
    2.33 +  author = {M. Stickel and R. Waldinger and M. Lowry and T. Pressburger and I. Underwood},
    2.34 +  title = {Deductive composition of astronomical software from subroutine libraries},
    2.35 +  pages = "341--355",
    2.36 +  crossref = {cade12}}
    2.37 +
    2.38  @book{suppes72,
    2.39    author	= {Patrick Suppes},
    2.40    title		= {Axiomatic Set Theory},
     3.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 07 15:16:40 2017 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Nov 07 15:16:41 2017 +0100
     3.3 @@ -57,6 +57,7 @@
     3.4    val iproverN : string
     3.5    val iprover_eqN : string
     3.6    val leo2N : string
     3.7 +  val leo3N : string
     3.8    val pirateN : string
     3.9    val satallaxN : string
    3.10    val snarkN : string
    3.11 @@ -126,6 +127,7 @@
    3.12  val iproverN = "iprover"
    3.13  val iprover_eqN = "iprover_eq"
    3.14  val leo2N = "leo2"
    3.15 +val leo3N = "leo3"
    3.16  val pirateN = "pirate"
    3.17  val satallaxN = "satallax"
    3.18  val snarkN = "snark"
    3.19 @@ -681,7 +683,7 @@
    3.20     >> map (core_inference z3_tptp_core_rule)) x
    3.21  
    3.22  fun parse_line local_name problem =
    3.23 -  if local_name = leo2N then parse_tstp_thf0_line problem
    3.24 +  if local_name = leo2N orelse local_name = leo3N then parse_tstp_thf0_line problem
    3.25    else if local_name = spassN then parse_spass_line
    3.26    else if local_name = pirateN then parse_pirate_line
    3.27    else if local_name = z3_tptpN then parse_z3_tptp_core_line
     4.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 07 15:16:40 2017 +0100
     4.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Nov 07 15:16:41 2017 +0100
     4.3 @@ -416,6 +416,29 @@
     4.4  val leo2 = (leo2N, fn () => leo2_config)
     4.5  
     4.6  
     4.7 +(* Leo-III *)
     4.8 +
     4.9 +(* include choice? Disabled now since its disabled for satallax as well. *)
    4.10 +val leo3_thf1 = THF (Polymorphic, THF_Without_Choice)
    4.11 +
    4.12 +val leo3_config : atp_config =
    4.13 +  {exec = K (["LEO3_HOME"], ["leo3"]),
    4.14 +   arguments = fn _ => fn full_proofs => fn _ => fn timeout => fn file_name => fn _ =>
    4.15 +     file_name ^ " " ^ "--atp cvc=$CVC4_SOLVER --atp e=\"$E_HOME\"/eprover \
    4.16 +     \-p -t " ^ string_of_int (to_secs 1 timeout) ^ " " ^
    4.17 +     (if full_proofs then "--nleq --naeq " else ""),
    4.18 +   proof_delims = tstp_proof_delims,
    4.19 +   known_failures = known_szs_status_failures,
    4.20 +   prem_role = Hypothesis,
    4.21 +   best_slices =
    4.22 +     (* FUDGE *)
    4.23 +     K [(1.0, (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), ""))],
    4.24 +   best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    4.25 +   best_max_new_mono_instances = default_max_new_mono_instances}
    4.26 +
    4.27 +val leo3 = (leo3N, fn () => leo3_config)
    4.28 +
    4.29 +
    4.30  (* Satallax *)
    4.31  
    4.32  (* Choice is disabled until there is proper reconstruction for it. *)
    4.33 @@ -431,7 +454,7 @@
    4.34     prem_role = Hypothesis,
    4.35     best_slices =
    4.36       (* FUDGE *)
    4.37 -     K [(1.0, (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    4.38 +     K [(1.0, (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), ""))],
    4.39     best_max_mono_iters = default_max_mono_iters - 1 (* FUDGE *),
    4.40     best_max_new_mono_instances = default_max_new_mono_instances}
    4.41  
    4.42 @@ -713,9 +736,12 @@
    4.43  val remote_leo2 =
    4.44    remotify_atp leo2 "LEO-II" ["1.5.0", "1.4", "1.3", "1.2", "1"]
    4.45      (K (((40, ""), leo2_thf0, "mono_native_higher", liftingN, false), "") (* FUDGE *))
    4.46 +val remote_leo3 =
    4.47 +  remotify_atp leo3 "Leo-III" ["1.1"]
    4.48 +    (K (((150, ""), leo3_thf1, "poly_native_higher", keep_lamsN, false), "") (* FUDGE *))
    4.49  val remote_satallax =
    4.50    remotify_atp satallax "Satallax" ["2.7", "2.3", "2"]
    4.51 -    (K (((60, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
    4.52 +    (K (((150, ""), satallax_thf0, "mono_native_higher", keep_lamsN, false), "") (* FUDGE *))
    4.53  val remote_vampire =
    4.54    remotify_atp vampire "Vampire" ["4.2", "4.1", "4.0"]
    4.55      (K (((400, ""), vampire_tff0, "mono_native", combs_or_liftingN, false), remote_vampire_full_proof_command) (* FUDGE *))
    4.56 @@ -766,10 +792,10 @@
    4.57    end
    4.58  
    4.59  val atps =
    4.60 -  [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
    4.61 +  [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, leo3, satallax, spass, vampire,
    4.62     z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
    4.63 -   remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
    4.64 -   remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
    4.65 +   remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_leo3, remote_satallax,
    4.66 +   remote_vampire, remote_snark, remote_pirate, remote_waldmeister, remote_waldmeister_new]
    4.67  
    4.68  val _ = Theory.setup (fold add_atp atps)
    4.69