# HG changeset patch # User desharna # Date 1605195869 -3600 # Node ID b6b6248d4719754b659716857d571c26f068a067 # Parent 56514a42eee836117d8461ba8b9355eb272f587b Tuned documentation diff -r 56514a42eee8 -r b6b6248d4719 src/Doc/Sledgehammer/document/root.tex --- a/src/Doc/Sledgehammer/document/root.tex Thu Nov 12 16:42:22 2020 +0100 +++ b/src/Doc/Sledgehammer/document/root.tex Thu Nov 12 16:44:29 2020 +0100 @@ -105,13 +105,13 @@ historical.} % The supported ATPs include agsyHOL \cite{agsyHOL}, Alt-Ergo \cite{alt-ergo}, E -\cite{schulz-2002}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III +\cite{schulz-2019}, iProver \cite{korovin-2009}, LEO-II \cite{leo2}, Leo-III \cite{leo3}, Satallax \cite{satallax}, 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 \cite{sutcliffe-2000}. The supported SMT solvers are CVC3 \cite{cvc3}, CVC4 \cite{cvc4}, veriT \cite{bouton-et-al-2009}, -and Z3 \cite{z3}. These are always run locally. +and Z3 \cite{de-moura-2008}. These are always run locally. The problem passed to the external provers (or solvers) consists of your current goal together with a heuristic selection of hundreds of facts (theorems) from the @@ -160,21 +160,21 @@ \begin{sloppy} \begin{enum} \item[\labelitemi] If you installed an official Isabelle package, it should -already include properly setup executables for CVC4, E, SPASS, Vampire, and Z3, -ready to use. To use Vampire, you must confirm that you are a noncommercial -user, as indicated by the message that is displayed when Sledgehammer is -invoked the first time. +already include properly set up executables for CVC4, E, SPASS, Vampire, veriT, +and Z3, ready to use. To use Vampire, you must confirm that you are a +noncommercial user, as indicated by the message that is displayed when +Sledgehammer is invoked the first time. \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC3, -CVC4, E, SPASS, Vampire, and Z3 binary packages from \download. Extract the -archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash etc\slash -components}% +CVC4, E, SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract +the archives, then add a line to your \texttt{\$ISABELLE\_HOME\_USER\slash +etc\slash components}% \footnote{The variable \texttt{\$ISABELLE\_HOME\_USER} is set by Isabelle at startup. Its value can be retrieved by executing \texttt{isabelle} \texttt{getenv} \texttt{ISABELLE\_HOME\_USER} on the command line.} -file with the absolute path to CVC3, CVC4, E, SPASS, Vampire, or Z3. For -example, if the \texttt{components} file does not exist yet and you extracted -SPASS to \texttt{/usr/local/spass-3.8ds}, create it with the single line +file with the absolute path to the prover. For example, if the +\texttt{components} file does not exist yet and you extracted SPASS to +\texttt{/usr/local/spass-3.8ds}, create it with the single line \prew \texttt{/usr/local/spass-3.8ds} @@ -203,7 +203,7 @@ variable \texttt{CVC3\_\allowbreak SOLVER}, \texttt{CVC4\_\allowbreak SOLVER}, \texttt{VERIT\_\allowbreak SOLVER}, or \texttt{Z3\_SOLVER} to the complete path of the executable, \emph{including the file name}. Sledgehammer has been tested -with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT smtcomp2019, and Z3 4.3.2. +with CVC3 2.2 and 2.4.1, CVC4 1.5-prerelease, veriT 2020.10-rmx, and Z3 4.3.2. Since Z3's output format is somewhat unstable, other versions of the solver might not work well with Sledgehammer. Ideally, also set \texttt{CVC3\_VERSION}, \texttt{CVC4\_VERSION}, \texttt{VERIT\_VERSION}, or @@ -247,8 +247,8 @@ \postw Instead of issuing the \textbf{sledgehammer} command, you can also use the -Sledgehammer panel in Isabelle/jEdit. Sledgehammer produces the following output -after a few seconds: +Sledgehammer panel in Isabelle/jEdit. Sledgehammer might produce something like +the following output after a few seconds: \prew \slshape @@ -267,9 +267,9 @@ provers are installed and how many processor cores are available, some of the provers might be missing or present with a \textit{remote\_} prefix. -For each successful prover, Sledgehammer gives a one-line \textit{metis} or -\textit{smt} method call. Rough timings are shown in parentheses, indicating how -fast the call is. You can click the proof to insert it into the theory text. +For each successful prover, Sledgehammer gives a one-line Isabelle proof. Rough +timings are shown in parentheses, indicating how fast the call is. You can +click the proof to insert it into the theory text. In addition, you can ask Sledgehammer for an Isar text proof by enabling the \textit{isar\_proofs} option (\S\ref{output-format}): @@ -279,8 +279,8 @@ \postw When Isar proof construction is successful, it can yield proofs that are more -readable and also faster than the \textit{metis} or \textit{smt} one-line -proofs. This feature is experimental and is only available for ATPs. +readable and also faster than \textit{metis} or \textit{smt} one-line +proofs. This feature is experimental. \section{Hints} @@ -448,15 +448,10 @@ versions of Metis. It is somewhat slower than \textit{metis}, but the proof search is fully typed, and it also includes more powerful rules such as the axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in -higher-order places (e.g., in set comprehensions). The method is automatically -tried as a fallback when \textit{metis} fails, and it is sometimes -generated by Sledgehammer instead of \textit{metis} if the proof obviously -requires type information or if \textit{metis} failed when Sledgehammer -preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with -various sets of option for up to 1~second each time to ensure that the generated -one-line proofs actually work and to display timing information. This can be -configured using the \textit{preplay\_timeout} and \textit{dont\_preplay} -options (\S\ref{timeouts}).) +higher-order places (e.g., in set comprehensions). The method is tried as a +fallback when \textit{metis} fails, and it is sometimes generated by +Sledgehammer instead of \textit{metis} if the proof obviously requires type +information or if \textit{metis} failed when Sledgehammer preplayed the proof. % At the other end of the soundness spectrum, \textit{metis} (\textit{no\_types}) uses no type information at all during the proof search, which is more efficient @@ -480,17 +475,18 @@ to Metis?} Orthogonally to the encoding of types, it is important to choose an appropriate -translation of $\lambda$-abstractions. Metis supports three translation schemes, -in decreasing order of power: Curry combinators (the default), +translation of $\lambda$-abstractions. Metis supports three translation +schemes, in decreasing order of power: Curry combinators (the default), $\lambda$-lifting, and a ``hiding'' scheme that disables all reasoning under $\lambda$-abstractions. The more powerful schemes also give the automatic -provers more rope to hang themselves. See the \textit{lam\_trans} option (\S\ref{problem-encoding}) for details. +provers more rope to hang themselves. See the \textit{lam\_trans} option +(\S\ref{problem-encoding}) for details. \point{Are the generated proofs minimal?} Automatic provers frequently use many more facts than are necessary. -Sledgehammer includes a minimization tool that takes a set of facts returned by +Sledgehammer includes a proof minimization tool that takes a set of facts returned by a given prover and repeatedly calls a prover or proof method with subsets of those facts to find a minimal set. Reducing the number of facts typically helps reconstruction, while decluttering the proof scripts. @@ -730,7 +726,7 @@ 1.5-prerelease. \item[\labelitemi] \textbf{\textit{e}:} E is a first-order resolution prover -developed by Stephan Schulz \cite{schulz-2002}. To use E, set the environment +developed by Stephan Schulz \cite{schulz-2019}. To use E, set the environment variable \texttt{E\_HOME} to the directory that contains the \texttt{eproof} executable and \texttt{E\_VERSION} to the version number (e.g., ``1.8''), or install the prebuilt E package from \download. Sledgehammer has been tested with @@ -747,27 +743,27 @@ higher-order prover developed by Christoph Benzm\"uller et al.\ \cite{leo2}, with support for the TPTP typed higher-order syntax (TH0). To use LEO-II, set the environment variable \texttt{LEO2\_HOME} to the directory that contains the -\texttt{leo} executable. Sledgehammer requires version 1.3.4 or above. +\texttt{leo} executable. Sledgehammer has been tested with version 1.3.4. \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 (TH0). 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. +\texttt{leo3} executable. Sledgehammer has been tested with version 1.1. \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 (TH0). To use Satallax, set the environment variable \texttt{SATALLAX\_HOME} to the directory that contains the -\texttt{satallax} executable. Sledgehammer requires version 2.2 or above. +\texttt{satallax} executable. Sledgehammer has been tested with version 2.2. \item[\labelitemi] \textbf{\textit{spass}:} SPASS is a first-order resolution prover developed by Christoph Weidenbach et al.\ \cite{weidenbach-et-al-2009}. To use SPASS, set the environment variable \texttt{SPASS\_HOME} to the directory that contains the \texttt{SPASS} executable and \texttt{SPASS\_VERSION} to the version number (e.g., ``3.8ds''), or install the prebuilt SPASS package from -\download. Sledgehammer requires version 3.8ds or above. +\download. Sledgehammer has been tested with version 3.8ds. \item[\labelitemi] \textbf{\textit{vampire}:} Vampire is a first-order resolution prover developed by Andrei Voronkov and his colleagues @@ -779,20 +775,20 @@ \item[\labelitemi] \textbf{\textit{verit}:} veriT \cite{bouton-et-al-2009} is an SMT solver developed by David D\'eharbe, Pascal Fontaine, and their colleagues. -It is specifically designed to produce detailed proofs for reconstruction in -proof assistants. To use veriT, set the environment variable -\texttt{VERIT\_SOLVER} to the complete path of the executable, including the -file name. Sledgehammer has been tested with version smtcomp2019. +It is designed to produce detailed proofs for reconstruction in proof +assistants. To use veriT, set the environment variable \texttt{VERIT\_SOLVER} +to the complete path of the executable, including the file name. Sledgehammer +has been tested with version 2020.10-rmx. \item[\labelitemi] \textbf{\textit{z3}:} Z3 is an SMT solver developed at -Microsoft Research \cite{z3}. To use Z3, set the environment variable +Microsoft Research \cite{de-moura-2008}. To use Z3, set the environment variable \texttt{Z3\_SOLVER} to the complete path of the executable, including the file name. Sledgehammer has been tested with a pre-release version of 4.4.0. \item[\labelitemi] \textbf{\textit{z3\_tptp}:} This version of Z3 pretends to -be an ATP, exploiting Z3's support for the TPTP typed first-order format -(TF0). It is included for experimental purposes. It requires version 4.3.1 of -Z3 or above. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME} +be an ATP, exploiting Z3's support for the TPTP typed first-order format (TF0). +It is included for experimental purposes. Sledgehammer has been tested with +version 4.3.1. To use it, set the environment variable \texttt{Z3\_TPTP\_HOME} to the directory that contains the \texttt{z3\_tptp} executable. \item[\labelitemi] \textbf{\textit{zipperposition}:} Zipperposition @@ -864,8 +860,8 @@ {\small See also \textit{verbose} (\S\ref{output-format}).} \optrue{minimize}{dont\_minimize} -Specifies whether the minimization tool should be invoked automatically after -proof search. +Specifies whether the proof minimization tool should be invoked automatically +after proof search. \nopagebreak {\small See also \textit{preplay\_timeout} (\S\ref{timeouts}) @@ -954,7 +950,7 @@ are relevant and 1 only theorems that refer to previously seen constants. \optrue{learn}{dont\_learn} -Specifies whether MaSh should be run automatically by Sledgehammer to learn the +Specifies whether Sledgehammer invocations should run MaSh to learn the available theories (and hence provide more accurate results). Learning takes place only if MaSh is enabled. @@ -1307,7 +1303,7 @@ sledgehammer[prover=e,prover_timeout=10] Huffman.thy \end{verbatim} -This command specifies Sledgehammer as the action, using E as the prover with a +This command specifies Sledgehammer as the action, using the E prover with a timeout of 10 seconds. The results are written to \texttt{output/Huffman.log}. \subsection{Example of Benchmarking Another Tool} diff -r 56514a42eee8 -r b6b6248d4719 src/Doc/manual.bib --- a/src/Doc/manual.bib Thu Nov 12 16:42:22 2020 +0100 +++ b/src/Doc/manual.bib Thu Nov 12 16:44:29 2020 +0100 @@ -587,6 +587,25 @@ publisher = CUP, year = 1990} +@inproceedings{de-moura-2008, + author = {Leonardo de Moura and + Nikolaj Bj{\o}rner}, + editor = {C. R. Ramakrishnan and + Jakob Rehof}, + title = {{Z3}: An Efficient {SMT} Solver}, + booktitle = {Tools and Algorithms for the Construction and Analysis of Systems --- TACAS 2008}, + series = {Lecture Notes in Computer Science}, + volume = {4963}, + pages = {337--340}, + publisher = {Springer}, + year = {2008}, + url = {https://doi.org/10.1007/978-3-540-78800-3\_24}, + doi = {10.1007/978-3-540-78800-3\_24}, + timestamp = {Tue, 14 May 2019 10:00:53 +0200}, + biburl = {https://dblp.org/rec/conf/tacas/MouraB08.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} + @Book{devlin79, author = {Keith J. Devlin}, title = {Fundamentals of Contemporary Set Theory}, @@ -1107,10 +1126,23 @@ title = {The Objective Caml system -- Documentation and user's manual}, note = {\url{http://caml.inria.fr/pub/docs/manual-ocaml/}}} -@misc{agsyHOL, - author = "Fredrik Lindblad", - title = "{agsyHOL}", - note = "\url{https://github.com/frelindb/agsyHOL}"} +@inproceedings{agsyHOL, + author = {Fredrik Lindblad}, + editor = {St{\'{e}}phane Demri and + Deepak Kapur and + Christoph Weidenbach}, + title = {A Focused Sequent Calculus for Higher-Order Logic}, + booktitle = {Automated Reasoning --- IJCAR 2014}, + series = {Lecture Notes in Computer Science}, + volume = {8562}, + pages = {61--75}, + publisher = {Springer}, + year = {2014}, + url = {https://doi.org/10.1007/978-3-319-08587-6\_5}, + doi = {10.1007/978-3-319-08587-6\_5}, + timestamp = {Tue, 14 May 2019 10:00:39 +0200}, + biburl = {https://dblp.org/rec/conf/cade/Lindblad14.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}} @incollection{lochbihler-2010, title = "Coinductive", @@ -1819,14 +1851,23 @@ number = 4 } -@article{schulz-2002, - author = "Stephan Schulz", - title = "E---A Brainiac Theorem Prover", - journal = "Journal of AI Communications", - year = 2002, - volume = 15, - number ="2/3", - pages = "111--126"} +@inproceedings{schulz-2019, + author = {Stephan Schulz and + Simon Cruanes and + Petar Vukmirovi\'c}, + editor = {Pascal Fontaine}, + title = {Faster, Higher, Stronger: {E} 2.3}, + booktitle = {Automated Deduction --- {CADE}-27}, + series = {Lecture Notes in Computer Science}, + volume = {11716}, + pages = {495--507}, + publisher = {Springer}, + year = {2019}, + url = {https://doi.org/10.1007/978-3-030-29436-6\_29}, + doi = {10.1007/978-3-030-29436-6\_29}, + timestamp = {Sat, 19 Oct 2019 20:28:03 +0200}, + biburl = {https://dblp.org/rec/conf/cade/0001CV19.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org}} @inproceedings{slind-tfl, author = {Konrad Slind}, @@ -2019,10 +2060,28 @@ note = {\url{http://x-symbol.sourceforge.net}} } -@misc{weidenbach-et-al-2009, - author = "Christoph Weidenbach and Dilyana Dimova and Arnaud Fietzke and Rohit Kumar and Martin Suda and Patrick Wischnewski", - title = "{SPASS} Version 3.5", - note = {\url{http://www.spass-prover.org/publications/spass.pdf}}} +@inproceedings{weidenbach-et-al-2009, + author = {Christoph Weidenbach and + Dilyana Dimova and + Arnaud Fietzke and + Rohit Kumar and + Martin Suda and + Patrick Wischnewski}, + editor = {Renate A. Schmidt}, + title = {{SPASS} Version 3.5}, + booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated + Deduction, Montreal, Canada, August 2-7, 2009. Proceedings}, + series = {Lecture Notes in Computer Science}, + volume = {5663}, + pages = {140--145}, + publisher = {Springer}, + year = {2009}, + url = {https://doi.org/10.1007/978-3-642-02959-2\_10}, + doi = {10.1007/978-3-642-02959-2\_10}, + timestamp = {Tue, 14 May 2019 10:00:39 +0200}, + biburl = {https://dblp.org/rec/conf/cade/WeidenbachDFKSW09.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} @manual{isabelle-system, author = {Makarius Wenzel}, @@ -2255,13 +2314,6 @@ title = {On the Implementation of an Extensible Declarative Proof Language}, crossref = {tphols99}} -%Z - -@misc{z3, - key = "Z3", - title = "Z3: An Efficient {SMT} Solver", - note = "\url{http://research.microsoft.com/en-us/um/redmond/projects/z3/}"} - % CROSS REFERENCES