--- 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.
--- 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},
--- 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
--- 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)