# HG changeset patch # User blanchet # Date 1304267844 -7200 # Node ID 3c1f302b3ee60ca752711cc6625b038a3477ef24 # Parent 46e690db16b8ccfdba1b43fbbf7d47c3e61a129e added support for ToFoF prover for experimenting with the TPTP TFF (typed first-order) format diff -r 46e690db16b8 -r 3c1f302b3ee6 doc-src/Sledgehammer/sledgehammer.tex --- a/doc-src/Sledgehammer/sledgehammer.tex Sun May 01 18:37:24 2011 +0200 +++ b/doc-src/Sledgehammer/sledgehammer.tex Sun May 01 18:37:24 2011 +0200 @@ -456,6 +456,12 @@ \item[$\bullet$] \textbf{\textit{remote\_vampire}:} The remote version of Vampire runs on Geoff Sutcliffe's Miami servers. Version 9 is used. +\item[$\bullet$] \textbf{\textit{remote\_tofof\_e}:} ToFoF-E is a metaprover +developed by Geoff Sutcliffe \cite{tofof} based on E running on his Miami +servers. This ATP supports a fragment of the TPTP many-typed first-order format +(TFF). It is supported primarily for experimenting with the +\textit{type\_sys} $=$ \textit{many\_typed} option (\S\ref{problem-encoding}). + \item[$\bullet$] \textbf{\textit{remote\_sine\_e}:} SInE-E is a metaprover developed by Kry\v stof Hoder \cite{sine} based on E. The remote version of SInE runs on Geoff Sutcliffe's Miami servers. @@ -575,7 +581,7 @@ This value implicitly enables \textit{monomorphize}. \item[$\bullet$] \textbf{\textit{many\_typed}:} Use the prover's support for -many-typed first-order logic logic if available; otherwise, fall back on +many-typed first-order logic if available; otherwise, fall back on \textit{mangled}. This value implicitly enables \textit{monomorphize}. \item[$\bullet$] \textbf{\textit{none}:} No type information is supplied to the diff -r 46e690db16b8 -r 3c1f302b3ee6 doc-src/manual.bib --- a/doc-src/manual.bib Sun May 01 18:37:24 2011 +0200 +++ b/doc-src/manual.bib Sun May 01 18:37:24 2011 +0200 @@ -650,7 +650,7 @@ @misc{sine, author = "Kry\v{s}tof Hoder", - title = "SInE (Sumo Inference Engine)", + title = "{SInE} (Sumo Inference Engine)", note = "\url{http://www.cs.man.ac.uk/~hoderk/sine/}"} @book{Hudak-Haskell,author={Paul Hudak}, @@ -1437,6 +1437,11 @@ year = 2000, publisher = Springer} +@misc{tofof, + author = "Geoff Sutcliffe", + title = "{ToFoF}", + note = "\url{http://www.cs.miami.edu/~tptp/ATPSystems/ToFoF/}"} + @Article{Sutter:2005, author = {H. Sutter}, title = {The Free Lunch Is Over --- A Fundamental Turn Toward Concurrency in Software}, diff -r 46e690db16b8 -r 3c1f302b3ee6 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:24 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Sun May 01 18:37:24 2011 +0200 @@ -33,6 +33,7 @@ val eN : string val spassN : string val vampireN : string + val tofof_eN : string val sine_eN : string val snarkN : string val z3_atpN : string @@ -75,6 +76,7 @@ val spassN = "spass" val vampireN = "vampire" val z3_atpN = "z3_atp" +val tofof_eN = "tofof_e" val sine_eN = "sine_e" val snarkN = "snark" val remote_prefix = "remote_" @@ -337,6 +339,8 @@ val remote_e = remotify_atp e "EP" ["1.0", "1.1", "1.2"] val remote_vampire = remotify_atp vampire "Vampire" ["0.6", "9.0", "1.0"] val remote_z3_atp = remotify_atp z3_atp "Z3---" ["2.18"] +val remote_tofof_e = + remote_atp tofof_eN "ToFoF" [] [] [] (K 200 (* FUDGE *)) true val remote_sine_e = remote_atp sine_eN "SInE" [] [] [(IncompleteUnprovable, "says Unknown")] (K 500 (* FUDGE *)) true @@ -365,7 +369,7 @@ Synchronized.change systems (fn _ => get_systems ()) val atps = [e, spass, vampire, z3_atp, remote_e, remote_vampire, remote_z3_atp, - remote_sine_e, remote_snark] + remote_tofof_e, remote_sine_e, remote_snark] val setup = fold add_atp atps end;