Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 8 Jul 1994 16:29:45 +0100 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA21590 for qed-out; Fri, 8 Jul 1994 10:12:24 -0500 Received: from altair (altair.mcs.anl.gov [140.221.2.7]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id KAA21582; Fri, 8 Jul 1994 10:12:11 -0500 From: Larry Wos Date: Fri, 8 Jul 1994 10:12:08 -0500 Message-Id: <199407081512.KAA22883@altair> To: dahn@mathematik.hu-berlin.de, qed@mcs.anl.gov Subject: valuable source Sender: owner-qed@mcs.anl.gov Precedence: bulk From atp_alias-request@cs.jcu.edu.au Fri Jul 8 09:53:36 1994 Received: from coral.cs.jcu.edu.au (geoff@coral.cs.jcu.edu.au [137.219.17.4]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id JAA21000; Fri, 8 Jul 1994 09:53:31 -0500 Received: (from geoff@localhost) by coral.cs.jcu.edu.au (8.6.7/8.6.6) id XAA01991; Fri, 8 Jul 1994 23:34:25 +1000 From: Geoff Sutcliffe Message-Id: <199407081334.XAA01991@coral.cs.jcu.edu.au> Subject: TPTP v1.1.1 Release To: ATP_alias@coral.cs.jcu.edu.au Date: Fri, 8 Jul 1994 23:34:24 +1000 (+1000) Cc: geoff@coral.cs.jcu.edu.au (Geoff Sutcliffe) X-Mailer: ELM [version 2.4 PL23] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 4655 Status: R The TPTP Problem Library, Release v1.1.1 ---------------------------------------- Geoff Sutcliffe Dep't of Computer Science, James Cook University, Australia. geoff@cs.jcu.edu.au Christian Suttner Institut fuer Informatik, TU Muenchen, Germany suttner@informatik.tu-muenchen.de The TPTP (Thousands of Problems for Theorem Provers) Problem Library is a library of test problems for automated theorem proving (ATP) systems, using the clausal normal form of 1st order logic. The TPTP supplies the ATP community with : + A comprehensive library of the ATP test problems that are available today, in order to provide an overview and a simple, unambiguous reference mechanism. + A comprehensive list of references and other interesting information for each problem. + New generalized variants of problems whose original presentation is hand- tailored towards a particular automated proof. + A utility to convert the problems to existing ATP formats. Currently the METEOR, MGTP, OTTER, PTTP, SETHEO, and SPRFN formats are supported, and the utility can easily be extended to produce any format required. + General guidelines outlining the requirements for ATP system evaluation. The principal motivation for this project is to move the testing and evaluation of ATP systems from the present ad hoc situation onto a firm footing. This is necessary, as results currently being published seldom provide an accurate reflection of the intrinsic power of the ATP system being considered. A common library of problems is necessary for meaningful system evaluations, meaningful system comparisons, repeatability of testing, and the production of statistically significant results. The TPTP is such a library. Release v1.1.1 of the TPTP is now available. TPTP v1.1.1 contains 2652 problems in 25 domains. Here's what's new in v1.1.1 : + The domain structure has been extended by two new domains in the field of engineering: CID (CIrcuit Design) and CIV (CIrcuit Verification). + There are 357 new problems (320 new abstract problems). + There have been 738 bugfixes done. + The tptp2X utility has been substantially overhauled. The utility can now apply a sequence of transformations to clauses, and installation has been simplified. + A list of registered users is included in the Documents directory. + The TPTP release and the release of the last bugfix are now given in the % File field of each problem and axiom set. The TPTP can be obtained by anonymous ftp from either the Department of Computer Science, James Cook University, Australia, or the Institut fuer Informatik, TU Muenchen, Germany. The ftp instructions are given below. There are three files, ReadMe-v1.1.1, TPTP-v1.1.1.tar.gz, and TR-v1.1.1.ps.gz. General information about the library is in the ReadMe-v1.1.1 file, the library is packaged in TPTP-v1.1.1.tar.gz, and a technical report describing the TPTP (in postscript form) is in TR-v1.1.1.ps.gz. Please read the ReadMe file, as it contains up-to-date information about the TPTP. The technical report serves as a manual explaining the structure and use of the TPTP. It also explains much of the reasoning behind the development of the TPTP. ----------------------------- ftp instructions -------------------------------- prompt> ftp coral.cs.jcu.edu.au #or: ftp 137.219.17.4 ftp flop.informatik.tu-muenchen.de #or: ftp 131.159.8.35 Name (coral.cs.jcu.edu.au:): ftp 331 Guest login ok, send your complete e-mail address as password. Password: ftp> cd pub/tptp-library ftp> get ReadMe-v1.1.1 ftp> binary ftp> get TPTP-v1.1.1.tar.gz ftp> get TR-v1.1.1.ps.gz ftp> quit ------------------------------------------------------------------------------- Convenient access to the TPTP is also available through the World Wide Web (WWW), using either of the following URLs : ftp://coral.cs.jcu.edu.au/web/cs/tptp.html http://wwwjessen.informatik.tu-muenchen.de/~suttner/tptp.html The TPTP is regularly updated with new problems, additional information, and enhanced utilities. If you would like to register as a TPTP user, and be kept informed of such developments, please email one of us. Our addresses are: Geoff Sutcliffe - geoff@cs.jcu.edu.au (FAX: +61-77-814029) or Christian Suttner - suttner@informatik.tu-muenchen.de (FAX: +49-89-526502)