# 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;