[SMT-LIB] TPTP and Automated Reasoning

Geoff Sutcliffe geoff at cs.miami.edu
Mon Oct 24 12:31:52 EDT 2016


Hi there,

Maybe you have heard of the TPTP project (www.tptp.org), and maybe you are 
a user of the TPTP resources, either directly or indirectly. Direct uses 
include downloading the TPTP library, using the SystemOnTPTP interface, and
being involved with CADE ATP System Competition (CASC). Indirect uses include 
using ATP systems whose development has benefited from direct use of the TPTP 
(Vampire, E, etc.), and using the Sledgehammer component of Isabelle (which 
calls the SystemOnTPTP service). If you appreciate what the TPTP does for
automated reasoning, this message is for you ...

                          The TPTP Needs Money

Please consider making a donation of 100 units of a reasonable currency, to 
support the TPTP. A donation can be made as an unrestricted gift (tax 
deductable) to the University of Miami, explicitly to support the TPTP and 
related projects. Details of how to do this now, easily, and with my gratitude,
are available on the TPTP web site, www.tptp.org

Cheers,

Geoff

Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Professor and Chairman                    Email : geoff at cs.miami.edu
Department of Computer Science            Phone : +1 305 2842158/2842268
University of Miami                       FAX   : +1 305 2842264
----- "My cat" is not a float. Every string should learn to swim. ------


More information about the SMT-LIB mailing list