tceic.com

学霸学习网 这下你爽了

学霸学习网 这下你爽了

¨ ¨ FAKULTAT FUR INFORMATIK

der Technischen Universitat Munchen ¨ ¨

Lehrstuhl VIII Forschungsgruppe Automated Reasoning

The TPTP Problem Library (TPTP v2.0.0)

Report AR-97-01

Suttner, C.B. Sutcli e, G.

Institut fur Informatik TU Munchen Germany

Department of Computer Science James Cook University Austraila

¨ ¨ TU Munchen, Arcisstr. 21, 80290 Munchen, Germany

The TPTP Problem Library

TPTP v2.0.0 { TR Date 6.6.97

Technical Report AR-97-01 Technical Report 97/042

1

Phone: +49-89-521098 Fax: +49-89-526502 Email: suttner@informatik.tu-muenchen.de

Christian B. Suttner 1 Institut fur Informatik TU Munchen, Germany

2 Department

Phone: +61 77 814622 Fax: +61-77-814029 Email: geo @cs.jcu.edu.au

Geo Sutcli e of Computer Science James Cook University, Australia

This report provides a detailed description of the TPTP Problem Library for automated theorem proving systems. This library is available via Internet, and forms a common basis for development of and experimentation with automated theorem provers. This report provides: the motivations for building the library; a discussion of the inadequacies of previous problem collections, and how these have been resolved in the TPTP; a description of the library structure, including overview information; descriptions of supplementary utility programs; guidelines for obtaining and using the library.

Abstract

Contents

1 Introduction

1.1 Previous Problem Collections . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2 What is Required? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1 2.2 2.3 2.4 2.5 2.6 The TPTP Domain Structure . . . . . . . . . . . Problem Versions and Standard Axiomatizations. Problem Generators . . . . . . . . . . . . . . . . Problem, Generator, and Axiomatization Naming Problem Presentation . . . . . . . . . . . . . . . Physical Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

2

3 5

2 Inside the TPTP

8 17 18 19 19 27 29 39

7

3 Utility Programs and Scripts 4 You and the TPTP

3.1 The tptp2X Utility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.2 The tptp1T Script . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.1 Quick Installation Guide . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 Important: Using the TPTP . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 Please contact us if ... . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.1 Current Activities . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Further Plans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

29 41

41 42 42

5 The Future

43

43 43 44

1

1 Introduction

The TPTP (Thousands of Problems for Theorem Provers) is a library of problems for Automated Theorem Proving (ATP) systems. The principal motivation for the TPTP project is to move the testing and evaluation of ATP systems from the previously ad hoc situation onto a rm footing. This became necessary, as results being published do not always accurately re ect the capabilities 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 signi cant results. The TPTP is such a library. The TPTP provides a simple, unambiguous source and reference mechanism for ATP problems. It is comprehensive and up-to-date, and thus provides an overview of the current application of ATP. The TPTP problems are stored in a speci cally designed, easy to understand format. A utility for manipulating the problems, and for converting the problems to other known ATP formats, is provided. A utility for nding problems with certain user speci ed characteristics is provided. Since its rst release in 1993, many researchers have used the TPTP as an appropriate and convenient basis for ATP system evaluation. A Quick Installation Guide for the TPTP is given in Section 4.1 on page 41. Please be sure to read the guidelines for using TPTP problems and presenting results, given in Section 4.2. This technical report explains the motivations and reasoning behind the development of the TPTP, and thus implicitly explains the design decisions made. It also serves as a manual explaining the structure and use of the TPTP: it provides a full description of the TPTP contents and organization, details of some utilities for manipulating the TPTP, and guidelines for obtaining and using the TPTP.

What's New in TPTP v2.0.0 (since v1.2.1): v2.0.0 is the second version of the

TPTP. The major changes in this release are : FOF (First Order Form) problems have been added. Three new domains have been added: FLD (Field theory), KRS (Knowledge Representation), and MGT (Management). Di culty ratings have been assigned to those problems for which su cient performance data from state-of-the-art ATP systems is available. The ratings are given in a new % Rating eld in the problem headers. A new utility called tptp1T, for nding problems with certain user speci ed characteristics, has been added. Other changes are given below. In the FOF part of the TPTP there are 110 new abstract problems, resulting in 217 new problems, in the domains COM GRP LCL MGT MSC PUZ SET SYN. In the CNF part of the TPTP there are 120 new abstract problems, resulting in 309 new problems, in the domains FLD KRS LCL PUZ. There is 1 new CNF generator, in the domain PUZ. There have been 3 bug xes done to CNF problems, in the domain GRP SYN. 2

The % Version elds have been reviewed. Problems that are Special have been explicitly labelled as such. The % Syntax eld of CNF problems has been extended to include the average number of literals per clause and the average term depth. The tptp2X utility has been extended and improved : ? Four new CNF output formats: CLIN-S, DFG, DIMACS, ILF. ? Three FOF output formats: TPTP, Otter, OSCAR. ? Nine new transformations: clausify (4 FOF to CNF transformations), simplify (simpli es a set of clauses), cnf (clausify then simplify), er (reverses arguments in the clauses of unit equality problems), ran er (does the er transformation to randomly selected clauses). ? The format modules now receive an extra argument containing the le header information. This information may be used only for supplementary documentation of the problem. The TPTP technical report (this document) has been updated.

1.1 Previous Problem Collections

A large number of interesting problems have accumulated over the years in the ATP community. Besides publishing particularly interesting individual problems, from early on researchers collected problems in order to obtain a basis for experimentation. Problems in FOF, published by mathematicians and logicians prior to the mechanization of reasoning, e.g. Chu56], provided the rst source for ATP researchers. The rst major publication1 in this regard was MOW76], which provides an explicit listing of clauses for 63 CNF problems, many of which are still relevant today. In the same year WM76] documented 86 CNF problems which have since commonly been used for ATP testing. The problem clauses are not supplied in WM76], however. A second major thrust was provided by Pel86], which lists 75 problems in both FOF and CNF. Other more recent papers are BLM+ 86], Qua92a], MW92], and McC93], to name a few. The Journal of Automated Reasoning's Problem Corner also provided interesting challenge problems. However, problems published in hardcopy form are often not suitable for testing ATP systems, because they have to be transcribed to electronic form. This is a cumbersome, error-prone process, and is feasible for only very small numbers of small problems. The sparsness of research into ATP systems for FOF problems meant that no electronic collections of FOF test problems have previously been commonly available. A CNF problem library in electronic form was made publicly available by Argonne National Laboratories (in Otter format, McC94]) in 1988 ANL]. This library has been a major source of problems for ATP researchers. Other electronic collections of CNF problems are available, but have not been announced o cially (e.g., that distributed with the SPRFN ATP system SPR]). Although some of these collections provide signi cant support to researchers, and formed the early core of the TPTP library, none (with the possible exception of the ANL library) was speci cally designed to serve as a common basis for ATP research. Rather, these collections typically were built in the course of research into a particular ATP system. As a result there are several factors that limit their usefulness as a common basis for research. In particular, previously existing problem collections

the late sixties.

1 To our knowledge,

the rst circulation of problems for testing ATP systems was due to Larry Wos in

3

are often hard to discover and obtain. System development and system evaluations typically rely on a small set of test problems, depending on the collections of problems available to the researcher. need to be transformed to the syntax of the ATP system being considered. The problem format used in a collection may not be appropriate for the desired purpose, and a comparatively large e ort is required just to make the problems locally usable (which in practice often means that such a collection of problems is simply ignored). are often limited in scope and size. The problems used are often homogeneous, and thus cannot be used for a broad test of the capabilities of the ATP system under consideration. If there are too few problems, statistically signi cant testing is not possible. may be outdated. The problems may insu ciently re ect the current state-of-the-art in ATP research. are sometimes designed and tuned (regarding formula selection, formula ordering, and formula structure) for a particular ATP system. Using a collection designed and tuned for a particular ATP system may lead to biases in results. provide no indication of the di culty or signi cance of the problems. The signi cance and di culty of a problem, with respect to the current state-ofthe-art in ATP systems, is hard to assess by newcomers to the eld. Existing test problems are often not adequate anymore (e.g., Schubert's Steamroller Sti86]), while others may be solvable only with specialized techniques (e.g., LIM+ Ble90]) and therefore are much too hard to start with. are inconsistent in their presentation of equally named problems. Many copies and variants of the same \original" problem may exist in di erent libraries. This means that unambiguous identi cation of problems, and therefore a clear interpretation of performance gures, for given problems, has become di cult. are usually undocumented. It is hard to obtain information on problem semantics, the original problem source, and the particular style of axiomatization. This also contributes to the problem of unambiguous problem identi cation. are almost always unserviced. They do not provide a mechanism for adding new problems or correcting errors in existing problems, and cannot be used to electronically distribute new and corrected problems to the ATP community. This in turn perpetuates the use of old and erroneous problems. provide no guidelines for their use. Quite often, inadequate system evaluations are performed. As a consequence, results that provide little indication of the system properties are reported. The problem of meaningfully interpreting results can be even worse than indicated. A few problems may be selected and hand-tuned (formulae arranged in a special way, irrelevant 4

formulae omitted, lemmas added in, etc) speci cally for the ATP system being tested. The presentation of a problem can signi cantly a ect the nature of the problem, and changing the formulae clearly makes a di erent problem altogether. Nevertheless the problem may be referenced under the same name as it was presented elsewhere. As a consequence the experimental results reveal little. Some researchers avoid this ambiguity by listing the formulae explicitly, but obviously this usually cannot be done for a large number of problems or for large individual problems. The only satisfactory solution to these issues is a common and stable library of problems. The TPTP is such a library.

1.2 What is Required?

The goal for building the TPTP has been to overcome previous drawbacks, and to centralize the burden of problem collection and maintenance. The TPTP tries to address all relevant issues. In particular, the TPTP is easy to discover and obtain. Awareness of the TPTP is assured by extensive formal and informal announcements. The TPTP is available by anonymous ftp, and is thus easily available to the research community. is easy to use. Problems are presented in a speci cally designed, easy to understand format. Automatic conversion to other known formats is also provided, thus eliminating the necessity for transcription. spans a diversity of subject matters. This reduces biases in the development and testing of ATP systems, which arise from the use of a limited scope of problems. It also provides an overview of the domains that ATP systems are used in. is large enough for statistically signi cant testing. In contrast to common practise, an ATP system should be evaluated over a large number of problems, rather than a small set of judiciously selected examples. The large size of the TPTP makes this possible. is comprehensive. The TPTP contains all problems known to the community. There is no longer a need to look elsewhere. is up-to-date. As new problems appear in the literature and elsewhere (see the paragraph Sources on page 7), they are added to the TPTP as soon as possible. is independent of any particular ATP system. The problems are arranged so as to be modular and human-readable, rather than arranged for a particular ATP system. contains problems varying in di culty, with a di culty rating for each problem. The di culty of problems in the TPTP ranges from very simple problems through to open problems. This allows all interested researchers, from newcomers to experts, to rely on the same problem library. The di culty ratings provided with each problem 5

are important for several reasons: (1) It simpli es problem selection according to the user's intention. (2) It allows the quality of an ATP system to be judged. (3) Over the years, changes in the problem ratings will provide an indicator of the advancement in ATP. provides statistics for each problem and the library as a whole. This provides information about the syntactic nature of the problems. has an unambiguous naming scheme. This provides unambiguous problem reference, and makes the comparison of results meaningful. See Section 2.4 for details. is well structured and documented. This allows e ective and e cient use of library. Useful background information, such as an overview of ATP application domains, is provided. documents each problem. This contributes to the unambiguous identi cation of each problem. provides a mechanism for adding new problems. The TPTP contains standard axiomatizations that can be used in new problems. This simpli es the construction of new problems (see Section 4.3). A template is provided for submission of new problems. The TPTP is thus a channel for making new problems available to the community, in a simple and e ective way. provides a mechanism for correcting errors in existing problems. All errors, noticed by the developers or reported by users, are corrected. Patched TPTP releases are made regularly. provides guidelines for its use in evaluating ATP systems. A standard library of problems together with evaluation guidelines makes reported results meaningful and reproducible by others. This will in turn simplify and improve system comparisons, and allow ATP researchers to accurately gauge their progress. The development of the TPTP problem library is an ongoing project, with the aim to provide all of the desired properties.

Current Limitations of the TPTP. The current release of the TPTP library is limited

to problems expressed in 1st order logic. There are no problems for induction, or for nonclassical theorem proving. However, see Section 5 for upcoming and planned extensions.

6

2 Inside the TPTP

Scope. Release v2.0.0 of the TPTP contains 202 abstract FOF problems, which result

in 217 FOF ATP problems (due to alternative presentations, see Section 2.2), and 2163 abstract CNF problems, which result in 3060 CNF ATP problems. Tables 1, 2, and 3 provide some overall statistics about the TPTP. Tables 4 and 5 provide some statistics about the non-propositional and propositional FOF problems. Tables 6 and 7 provide some statistics about the non-propositional and propositional CNF problems. Number of problem domains Number of abstract problems Number of generic problems Number of problems Number of propositional problems Number of problems with equality Number of pure equality problems Number of standard problems 28 2268 87 3277 61 (1%) 1963 (59%) 496 (15%) 1899 (57%)

Table 1: Statistics on the TPTP. Number of problem domains 8 Number of abstract problems 202 Number of generic problems 1 Number of problems 217 Number of propositional problems 19 (8%) Number of problems with equality 44 (20%) Number of pure equality problems 4 (1%) Number of standard problems 56 (25%) Table 2: Statistics on the FOF part of the TPTP. The problems in the TPTP are syntactically diverse, as is indicated by the ranges of the values in Tables 4-7. The problems in the TPTP are also semantically diverse, as is indicated by the range of domains that are covered. The problems are grouped into domains, covering topics in the elds of logic, mathematics, computer science, engineering, social sciences, and others. The domains are presented and discussed in Section 2.1. sources have been existing electronic problem collections and the ATP literature. Other sources include logic programming, mathematics, puzzles, and correspondence with ATP researchers. Many people and organizations have contributed towards the TPTP: the foundations of the TPTP were laid with David Plaisted's SPRFN collection; many problems have been taken from Argonne National Laboratory's ATP problem library (special thanks to Bill McCune here); Art Quaife provided several hundred problems in set theory and algebra; the Journal of Automated Reasoning, CADE Proceedings, and Association 7

Sources. The problems have been collected from various sources. The two principal

Number of problem domains Number of abstract problems Number of generic problems Number of problems Number of propositional problems Number of non-Horn problems Number of range restricted problems Number of problems with equality Number of pure equality problems Number of unit equality problems Number of satis able problems Number of standard problems

27 2163 86 3060 42 1791 399 1919 492 376 46 1843

(1%) (58%) (13%) (62%) (16%) (12%) (1%) (60%)

Table 3: Statistics on the CNF part of the TPTP. for Automated Reasoning Newsletters have provided a wealth of material; smaller numbers of problems have been provided by a number of further contributors (see the Acknowledgements at the end of Section 5). xed releases are made. Each release of the TPTP is identi ed by a release number, in the form v<Version>.<Edition>.<Patch level>. The Version number enumerates major new releases of the TPTP, in which important new features have been added. The Edition number is incremented each time new problems are added to the current version. The Patch level is incremented each time errors, found in the current edition, are corrected. All non-trivial changes are recorded in a history le, as well as in the le for an a ected problem.

Releases. The TPTP is managed in the manner of a software product, in the sense that

2.1 The TPTP Domain Structure

This section provides the structure according to which the problems are grouped into domains. Some information about the domains is also given. An attempt has been made to classify the totality of the TPTP problems in a systematic and natural way. The resulting domain scheme re ects the natural hierarchy of scienti c domains, as presented in standard subject classi cation literature. The current classication is based mainly on the Dewey Decimal Classi cation (DDC) Dew89] and the Mathematics Subject Classi cation (MSC) MSC92] used for the Mathematical Reviews by the American Mathematical Society. Five main elds are de ned: logic, mathematics, computer science, engineering, and other. Each eld contains further subdivisions, called domains. Each domain is identi ed by a three-letter mnemonic. These mnemonics are also part of the TPTP problem naming scheme (see Section 2.4). The TPTP domains constitute the basic units of the classi cation. The full classi cation scheme is shown in Figure 1, and the number of Abstract problems, problems, and generic problems in each domain is shown in Table 8. 8

Measure Minimum Maximum Average Median Number of formulae 1 53 7 1 Percentage of unit formulae 0% 75% 5% 0% Number of atoms 2 159 25 8 Percentage of equality atoms 0% 100% 10% 0% . . . in equality problems 26% 100% 46% 39% Average atoms per formula 1.5 20.0 4.8 4.0 Maximal formula depth 3 15 6 6 Average formula depth 1 12 5 5 Number of connectives 1 110 18 7 ~ 0 9 0 0 | 0 6 0 0 & 0 52 8 2 <=> 0 11 0 0 => 0 51 7 3 <= 0 0 0 0 <~> 0 1 0 0 ~| 0 0 0 0 ~& 0 0 0 0 Number of predicate symbols 1 17 3 2 Percentage of propositions 0% 50% 2% 0% Minimal predicate arities 0 5 1 1 Maximal predicate arities 1 5 2 2 Number of functors 0 11 1 0 Percentage of constants 0% 100% 15% 0% Minimal functor arities 0 2 0 0 Maximal functor arities 0 3 0 0 Number of variables 1 143 21 5 Percentage of singletons 0% 100% 25% 2% ! 0 143 19 3 ? 0 11 1 2 Maximal term depth 1 4 1 1 Average term depth 1 1 1 1 Table 4: Statistics for non-propositional FOF problems.

9

Logic Mathematics

Computer science

Engineering Social Science Other

Combinatory logic Logic calculi Henkin models Set Theory Graph Theory Algebra Boolean Algebra Robbins Algebra Left distributive Lattices Groups Rings General Algebra Number Theory Topology Analysis Geometry Field Theory Category theory Computing Theory Knowledge Representation Schemes Planning Program Veri cation Circuit Design Circuit Veri cation Management Syntactic Puzzles Miscellaneous

COL LCL HEN SET GRA BOO ROB LDA LAT GRP RNG ALG NUM TOP ANA GEO FLD CAT COM KRS PLA PRV CID CIV MGT SYN PUZ MSC

Figure 1: The domain structure of the TPTP.

10

Measure Number of formulae Percentage of unit formulae Number of atoms Average atoms per formula Maximal formula depth Average formula depth Number of connectives

Minimum Maximum Average Median 1 4 1 1 0% 0% 0% 0% 2 10 5 4 2.0 10.0 4.8 4.0 2 10 4 4 2 10 4 4 1 12 5 5 ~ 0 5 1 1 | 0 4 1 1 & 0 2 0 0 <=> 0 9 1 1 => 0 3 1 1 <= 0 0 0 0 <~> 0 0 0 0 ~| 0 0 0 0 ~& 0 0 0 0 Number of predicate symbols 1 5 2 2 Table 5: Statistics for propositional FOF problems. A brief description of the domains, with a non-ATP reference for a general introduction and a generic ATP reference, is given below. For each domain, appropriate DDC and MSC numbers are also given: ALG Algebra. An algebra is a set with a system of operations de ned on it. Indices : DDC 512; MSC 06XX, 20XX. References : General Bou89, BM65, BB70], ATP {. ANA Analysis. Analysis is a branch of mathematics concerned with functions and limits. The main parts of analysis are di erential calculus, integral calculus, and the theory of functions. Indices : DDC 515; MSC 26XX. References : General Ros90], ATP Ble90]. BOO Boolean Algebra. A Boolean algebra is a set of elements with two binary operations which are idempotent, commutative, and associative. These operations are mutually distributive, there exist universal bounds 0; 1, and there is a unary operation of complementation. Indices : DDC 511.324, 512.89; MSC 06EXX. References : General Whi61, BM65, BB70], ATP {. CAT Category Theory. A category is a mathematical structure together with the morphisms that preserve this structure. Indices : DDC 512.55; MSC 18XX. 11

Measure Minimum Maximum Average Median Number of clauses 2 504 109 35 Percentage of non-Horn clauses 0% 99% 6% 4% . . . in non-Horn problems 2% 99% 9% 6% Percentage of unit clauses 0% 100% 33% 22% Percentage of range restricted clauses 0% 100% 64% 63% Number of literals 2 1512 253 83 Percentage of equality literals 0% 100% 39% 45% . . . in equality problems 19% 100% 61% 47% Maximal clause size 1 25 4 5 Average clause size 1 8 1 2 Number of predicate symbols 1 48 8 3 Percentage of propositions 0% 67% 0% 0% Minimal predicate arities 0 20 1 1 Maximal predicate arities 1 20 2 3 Number of functors 1 93 21 9 Percentage of constants 0% 100% 51% 50% Minimal functor arities 0 2 0 0 Maximal functor arities 0 8 2 2 Number of variables 0 1094 247 73 Percentage of singletons 0% 100% 7% 6% Maximal term depth 1 14 4 4 Average term depth 1 4 1 1 Table 6: Statistics for non-propositional CNF problems.

Measure Minimum Maximum Average Median Number of clauses 3 82 24 18 Percentage of non-Horn clauses 0% 81% 25% 25% . . . in non-Horn problems 8% 81% 35% 33% Percentage of unit clauses 0% 100% 19% 13% Number of literals 4 232 64 40 Maximal clause size 1 11 3 3 Maximal clause size 1 11 3 3 Average clause size 1 5 1 2 Average clause size 1 5 1 2 Number of predicate symbols 2 63 13 11 Table 7: Statistics for propositional CNF problems. 12

Total FOF CNF Dom Abs. Probs. Gen. Abs. Probs. Gen. Abs. Probs. Gen. ALG 2 4 0 0 0 0 2 4 0 ANA 5 19 0 0 0 0 5 19 0 BOO 19 52 0 0 0 0 19 52 0 CAT 19 58 0 0 0 0 19 58 0 CID 3 4 0 0 0 0 3 4 0 CIV 4 4 0 0 0 0 4 4 0 COL 80 140 0 0 0 0 80 140 0 COM 4 9 0 1 3 0 4 6 0 FLD 100 281 0 0 0 0 100 281 0 GEO 78 165 0 0 0 0 78 165 0 GRA 1 1 0 0 0 0 1 1 0 GRP 194 314 50 1 1 0 193 313 50 HEN 12 64 0 0 0 0 12 64 0 KRS 17 17 0 0 0 0 17 17 0 LAT 5 10 0 0 0 0 5 10 0 LCL 257 281 0 2 2 0 257 279 0 LDA 14 23 0 0 0 0 14 23 0 MGT 41 53 0 41 53 0 0 0 0 MSC 9 13 3 1 1 0 9 12 3 NUM 285 309 2 0 0 0 285 309 2 PLA 23 30 0 0 0 0 23 30 0 PRV 9 9 0 0 0 0 9 9 0 PUZ 36 57 4 2 2 0 36 55 4 RNG 40 100 0 0 0 0 40 100 0 ROB 27 36 0 0 0 0 27 36 0 SET 562 700 0 5 5 0 562 695 0 SYN 403 500 28 149 150 1 340 350 27 TOP 19 24 0 0 0 0 19 24 0 Table 8: TPTP Domain Sizes.

13

CID

CIV

COL

COM

FLD

GEO

GRA

GRP

References : General Mac71], ATP MOW76]. Circuit Design. Circuits are formed by inter-connecting logic gates. Circuit design is used to form a circuit that will transform given input patterns to required output patterns. Indices : DDC 621.395; MSC 94CXX. References : General Hay93], ATP WW83]. Circuit Veri cation. Circuit veri cation is used to ensure that a previously designed circuit performs the desired transformation of input patterns to required output patterns. One approach is to check the performance of the circuit for every possible combination of given inputs. Other techniques are also used. Indices : DDC 621.395; MSC 94CXX. References : General Hay93], ATP Woj83]. Combinatory Logic. Combinatory logic is about applying one function to another. It can be viewed as an alternative foundation of mathematics (or, due to its Turing-completeness, as a programming language). More formally, it is a system satisfying two combinators and satisfying re exivity, symmetry, transitivity, and two equality substitution axioms for the function that exists implicitly for applying one combinator to another. Indices : DDC 510.101; MSC 03B40. References : General CF58, CHS72, Bar81], ATP WM88]. Computing Theory. Computing theory is a sub eld of computer science dealing with theoretical issues such as decidability (whether or not a given problem admits an algorithmic solution), completeness (does an algorithm always nd a solution if one exists?), correctness (are only solutions produced?), and computational complexity (the resource requirements of algorithms). Indices : DDC 004-006; MSC 68XX. References : General HU79], ATP {. Field Theory. A eld is ring (see below) in which the * operation is commutative, and for which there is an identity element in G, and for which each non-identity element of G has an inverse in G. Indices : DDC 512.32; MSC 12XX. References : General Ada82], ATP Dra93]. Geometry. Geometry is a branch of mathematics that deals with the measurement, properties, and relationships of points, lines, angles, surfaces, and solids. In the TPTP the Geometry domain deals mainly with plane geometry, based on Tarski's axiom system for Euclidean geometry. Indices : DDC 516; MSC 51. References : General Tar51, Tar59], ATP Qua92b]. Graph Theory. A graph consists of a nite non-empty set of points together with a prescribed set of pairs of points. Indices : DDC 510.09; MSC 05CXX, 68R10. References : General Har69, BB70], ATP {. Group Theory. 14

HEN

KRS

LAT

LCL

LDA

MGT

A group is a set G and a binary operation +:GxG!G which is associative, and for which there is an identity element in G, and for which each element of G has an inverse in G. Indices : DDC 512.2; MSC 20 References : General Bou89, BM65], ATP MOW76]. Henkin Models. Henkin models provide a generalized semantics for higher order logics. This leads to a larger class of models and, as a consequence, fewer true sentences. However, in contrast to standard semantics, complete and correct calculi can be found. Indices : DDC 160; MSC 03CXX. References : General Hen50, Leb83], ATP {. Knowledge Representation. Knowledge Representation is concerned with writing down descriptions such that the descriptions can be manipulated by a machine. Indices : DDC 006.3; MSC 68T30. References : General BL85, CM87], ATP {. Lattice Theory. A lattice is a set of elements, with two binary operations which are idempotent, commutative, and associative, and which satisfy the absorption law. Indices : DDC 512.865; MSC 06BXX. References : General BM65], ATP McC88]. Logic Calculi. A logic calculus de nes axioms and rules of inference that can be used to prove theorems. This domain currently contains the following logical calculi: ? Implication/Negation 2 valued modal ? Implication/Negation 2 valued sentential (CN-calculus) ? Implicational propositional (IC-calculus, negation-free part of sentential calc.) ? Implication/Falsehood 2 valued sentential (C0-calculus) ? Disjunction/Negation 2 valued sentential (AN-calculus) ? Many valued sentential (MV-calculus) ? Equivalential (EC-calculus, theorems represent group identity in Boolean groups) ? R (under some constraint, theorems represent identity in Abelian groups) ? Left group (LG-calculus, under some constraint theorems represent formulas equal to identity in groups) ? Right group (RG-calculus, theorems are related to identity in groups) ? Wajsberg Algebra. Indices : DDC 511.3; MSC 03XX. References : General Luk63], ATP MW92]. Left Distributive Algebra. LD-algebras are related to large cardinals. Under a very strong large cardinal assumption, the free-monogenic LD-algebra can be represented by an algebra of elementary embeddings. Theorems about this algebra can be proved from a small number of properties, suggesting the de nition of an embedding algebra. Indices : DDC 512; MSC 20N02, 03E55, 08B20 References : General {, ATP Jec93]. Management. Management is the study of systems, and their use and production of resources. 15

MSC NUM PLA

PRV

PUZ RNG

ROB

SET

SYN TOP

Indices : DDC 302-303; MSC 90XX. References : General {, ATP PM94, PBMON94]. Miscellaneous. A collection of problems which do not t well into any other domain. Number Theory. Number theory is the study of integers and their properties. Indices : DDC 512.7; MSC 11YXX. References : General HW92], ATP Qua92b]. Planning. Planning is the process of determining the sequence of actions to be performed by an agent, to reach a desired state. The initial state and the desired state are provided. Indices : DDC 006.3; MSC 68T99. References : General AKPT91], ATP Pla81, Pla82]. Program Veri cation. Program veri cation formally establishes that a computer program does the task it is designed for. Indices : DDC 005.14; MSC 68Q60. References : General {, ATP WOLB92, MOW76]. Puzzles. Puzzles are designed to test the ingenuity of humans. Indices : DDC 510, 793.73; MSC {. References : General Car86, Smu78b, Smu78a], ATP {. Ring Theory. A ring is a group (see above) in which the binary operation is commutative, with an associative and distributive operation *:GxG!G for which there is an identity element in G. Indices : DDC 512.4; MSC 13XX, 16XX. References : General Bou89, BB70], ATP MOW76]. Robbins Algebra. The Robbin Algebra domain revolves around the question \Is every Robbins algebra Boolean?". Most of the problems in this domain identify conditions that make a near-Boolean algebra Boolean. Indices : DDC 512; MSC 03G15. References : General HMT71], ATP Win90]. Set Theory. Classically, a set is a totality of certain de nite, distinguishable objects of our intuition or thought - called the elements of the set. Due to paradoxes that arise from such a naive de nition, mathematicians now regard the notion of a set as an unde ned, primitive concept How72]. In this domain, Naive and NeumannBernays-Godel axiom sets are used. Indices : DDC 511.322, 512.817; MSC 03EXX, 04XX. References : General Neu25, Qui69], ATP Qua92b]. Syntactic. Syntactic problems have no obvious semantic interpretation. Indices : DDC {; MSC {. References : General Chu56], ATP Pel86]. Topology. 16

Topology is the study of properties of geometric con gurations (e.g., point sets) which are unaltered by elastic deformations (homeomorphisms, i.e., functions that are 1-1 mappings between sets such that both the function and its inverse are continuous). Indices : DDC 514; MSC 46AXX. References : General Kel55, Mun75], ATP WM89].

2.2 Problem Versions and Standard Axiomatizations.

There are often many ways to formulate a problem for presentation to an ATP system. Thus, in the TPTP, there are often alternative presentations of a problem. The alternative presentations are called versions of the underlying abstract problem. As the problem versions are the objects that ATP systems must deal with, they are referred to simply as problems, and the abstract problems are referred to explicitly as such. Each problem is stored in a separate physical le. In the TPTP the most coarse grain di erentiation between problem versions is whether the problem is presented in FOF or CNF. Within a given presentation, the primary reason for di erent versions of an abstract problem is the use of di erent axiomatizations. This issue is discussed below. A secondary reason is di erent formulations of the theorem to be proved, e.g., di erent clausal forms of a FOF problem. Commonly, many di erent axiomatizations of a theory exist. In the TPTP an axiomatization is standard if it is a complete axiomatization of an established theory, and it has not had any lemmas added. (Note: A standard axiomatization may be redundant, because some axioms are dependent on others. In general, it is not known whether or not an axiomatization is minimal, and thus the possibility of redundancy in standard axiomatizations must be tolerated.) In the TPTP, standard axiomatizations are kept in separate axiom les, and are included in problems as appropriate. By using di erent standard axiomatizations of a particular theory, di erent versions of a problem can be formed. Sets of specialization axioms may be used to extend or constrain an axiomatization. Specialization axioms are also kept in separate axiom les. If an axiomatization uses equality, the required axioms of substitution are kept separate from the theory speci c axioms. The equality axioms of re exivity, symmetry, and transitivity, which are also required when equality is present, are also kept separately. A side e ect of separating out the axioms into axiom les is that the formula order in the TPTP presentation of problems is typically di erent from that of any original presentation. This reordering is acceptable because the performance of a decent ATP system should not be very dependent on a particular formula ordering in the TPTP. Within the ATP community, some problems have been created with non-standard axiomatizations. A non-standard axiomatization is formed by modifying a standard axiomatization. The standard axiomatization may be reduced (i.e., axioms are removed) and the result is an incomplete axiomatization, or it may be augmented (i.e., lemmas are added) and the result is a redundant axiomatization. Non-standard axiomatizations are typically used to nd a proof of a theorem (based on the axiomatization) using a particular ATP system. In any 'real' application of an ATP system, a standard axiomatization of the application domain would typically have to be used, at least initially. Thus the use of 17

Di erent Axiomatizations

standard axiomatizations is desirable, because it re ects such 'real' usage. In the TPTP, for each collected problem that uses a non-standard axiomatization, a new version of the problem is created with a standard axiomatization. The axioms in some TPTP problems do not capture any established theory, i.e., a standard axiomatization cannot exist. These axiomatizations are called special axiomatizations. Typically, such axiomatizations are used in only one problem. In the TPTP equality is represented using the equal/2 predicate, written in pre x notation like all other predicates. The equal/2 predicate is used only if the equality axiomatization in the problem is complete, i.e., including the axioms of re exivity, symmetry, transitivity, function substitution for all functors, and predicate substitution for all predicate symbols. If the equality axiomatization is not complete, but the 'intention' is to represent equality, the equalish/2 predicate is used. The TPTP problems containing the equal/2 predicate contain a complete equality axiomatization. Many ATP systems have built in mechanisms, e.g., paramodulation, that make some or all of the equality and substitution axioms unnecessary. If any of these axioms are removed when the problems are submitted to an ATP system, then the removal must be explicitly noted in reported results (see Section 4.2). The tptp2X utility (see Section 3.1) can be used to remove equality axioms.

Equality Axiomatization

2.3 Problem Generators

Some abstract problems have a generic nature, and particular instances of the abstract problem are formed according to some size parameter(s). An example of a generic problem is the N ?queens problem: place N queens on a N N chess board such that no queen attacks another. The formulae for any size of this problem can be generated automatically, for any size of N 2. Note that satis ability may depend on the problem size. Up to TPTP v1.1.3, the TPTP contained problem les for particular sizes of generic problems. This, however, was undesirable. Firstly, only a nite number of di erent problem sizes could be included, and therefore a desired size may have been missing. Secondly, even a small number of di erent problem sizes for each generic problem could consume a considerable amount of disk space. To overcome these problems the TPTP now contains generator les. Generator les are used to generate instances of generic problems, according to user supplied size parameters. The generators are used in conjunction with the tptp2X utility, and a full description of their use is given in Section 3.1. For convenience, the TPTP still contains a particular instance of each generic problem. The TPTP size chosen for each such instance is a compromise between being large enough to be non-trivial for the SETHEO ATP system LSBB92] and small enough to avoid using too much disk space. An unsatis able size is chosen whereever one exists. As result data for other systems are obtained, these sizes might change in order to remove the current bias towards the SETHEO system. The statistics in Tables 1-7 take into account these instances of generic problems.

18

2.4 Problem, Generator, and Axiomatization Naming

Providing unambiguous names for all problems is necessary in a problem library. A naming scheme has been developed for the TPTP, to provide unique, stable names for abstract problems, problems, generators, and axiomatizations. Files are assigned names according to the schemes depicted in Figures 2 and 3. The DDDNNN combination provides an unambiguous name for an abstract problem or axiomatization. The DDDNNNFV .SSS] combination provides an unambiguous name for a problem or generator, and the DDDNNNFE combination provides an unambiguous name for a group of axioms. The complete le names are unique within the TPTP.

F V : S S S ]: T | {z } | {z } |{z} |{z} | {z } |{z} DDD N N N

File name extension. An extension p denotes a problem le, and an extension g denotes a generator le. Size parameter(s). These only occur for generated problems, and give the size parameter(s). Version number. It di erentiates between di erent versions of the abstract problem, as discussed in Section 2.2. Form. - for CNF and + for FOF. Abstract problem number. It is unique within the domain. Domain name abbreviation. The domain names and their abbreviations are listed in Figure 1.

Figure 2: Problem le naming scheme. The abstract problem numbers within each domain are not always successive. This is because some numbers have already been allocated to problems that will be part of a future TPTP release (see Section 5.1). The version numbers used for each abstract problem do not always start at 1, and are not always successive. This is because the same version number is assigned (whereever possible) to all problems that come from the same source, within each domain. If a le is ever removed from or renamed in the TPTP, then the extension is changed to .rm. The le is not physically removed, and a comment is added to the le to explain what has happened. This mechanism maintains the unique identi cation of problems and axiomatizations.

2.5 Problem Presentation

The physical presentation of the TPTP problem library is such that ATP researchers can easily use the problems. The TPTP le format, for problem les and axiom les, has three main sections. The rst section is a header section that contains information for the user. This information is not for use by ATP systems (see Section 4.2). The second section contains include instructions for axiom les. The last section contains the formulae that are speci c to the problem or axiomatization. TPTP generator les have three sections, di erent from the problem and axiom les. The header section of generator les is similar to that of problem and axiom les, but with place-holders for information that is lled in 19

DDD N N N

| {z } | {z } |{z} |{z} |{z}

F

E

: TT

File name extension, one of ax or eq. An extension ax denotes a le containing axioms speci c to a theory. An extension eq denotes a le containing equality substitution axioms for the corresponding theory speci c axioms. Specialization number. It identi es groups of axioms that are used to specialize an axiomatization. Axiomatizations of basic theories are allocated the number 0, and specialization axiom groups are numbered from 1 onwards. Form. - for CNF and + for FOF. Axiomatization number. It is unique within the domain. Domain name abbreviation. The domain names and their abbreviations are listed in Figure 1.

Figure 3: Axiom le naming scheme. based on the size of problem and the formulae generated. Following that comes Prolog source code to generate the formulae, and nally data describing the permissible sizes and the chosen TPTP size for the problem. More details are given in Section 3.1.7. The syntax of all les is that of Prolog. This conformance makes it trivial to manipulate the les using Prolog. All information in the les that is not for use by ATP systems is formatted as Prolog comments, with a leading %. All the information for ATP systems is formatted as Prolog facts. The tptp2X utility can be used to convert TPTP les to other known ATP system formats (see Section 3.1). A description of the information contained in TPTP les is given below.

2.5.1 The Header Section

This section contains information about the problem, for the user. It is divided into four parts. The rst part identi es and describes the problem. The second part provides information about occurrences of the problem. The third part gives the problem's ATP status and a table of syntactic measurements made on the problem. The last part contains general information about the problem. Examples of TPTP headers, extracted from the problem les GRP194+1.p and GRP039-7.p, are shown in Figures 4 and 5.

The % File eld. This eld contains three items of information. The rst item is the problem's name. This is displayed in the format <Abstract problem name>-|+<Problem version> .<Size>]. The current TPTP release number is given next, followed by the TPTP release in which the problem was released or last bug xed (i.e., the formulae were changed). The abstract problem name in Figure 5 is GRP039, the - indicates that the problem is presented in CNF, and the problem version is 7. The TPTP release is v1.2.1, and the problem clauses were last bug xed in release v1.0.1.

from which the problem is drawn (see Section 2.1). The domain corresponds to the rst 20

The %

Domain

eld. The domain eld identi es the domain, and possibly a subdomain,

%-------------------------------------------------------------------------% File : GRP194+1 : TPTP v2.0.0. Released v2.0.0. % Domain : Group Theory (Semigroups) % Problem : In semigroups, a surjective homomorphism maps the zero % Version : Goller, 1993] axioms. % English : If (F,*) and (H,+) are two semigroups, phi is a surjective % homomorphism from F to H, and id is a left zero for F, % then phi(id) is a left zero for H. % Refs % % % Source % Names % Status % Rating % Syntax % % % % % % % % % : Goller C. (1993), Anwendung des Theorembeweisers SETHEO auf die Theorie der Halbgruppen und Gruppen, Report FKI-174-93, Technische Universitaet Muenchen, Munich Germany. : Goller, 1993] : : theorem : ? v2.0.0 : Number of formulae Number of atoms Maximal formula depth Number of connectives

: : : :

19 47 6 28

Number of predicates Number of functors Number of variables Maximal term depth

: : : :

3 5 47 3

( ( ( ( ( ( ( ( ( (

3 22 3 0 1 0 0 3 0 1

unit) equality) average) ~ ; 0 |; 11 &) <=>; 16 =>; 0 <=) <~>; 0 ~|; 0 ~&) propositional; 2-2 arity) constant; 0-3 arity) singleton; 46 !; 1 ?) average)

% Comments : %--------------------------------------------------------------------------

Figure 4: Example of a FOF problem le header (GRP194+1.p). three letters of the problem name. The domain of the problem of Figure 5 is Theory, and the subdomain is Subgroups.

Group

The % Problem eld. This eld provides a one-line, high-level description of the abstract problem. In axiom les, this eld is called % Axioms, and provides a one-line, high-level description of the axiomatization. Thus, the problem of Figure 5 proves that Subgroups of index 2 are normal. The % Version eld. This eld gives information that di erentiates this version of the problem from other versions of the problem. The rst possible di erentiation is the axiomatization that is used. If a speci c axiomatization is used, a citation is provided. In the problem of Figure 5, the axiomatization used is that of McCharen, et al., 1976]. If the axiomatization is a pure equality axiomatization (uses only the equal/2 predicate) then this is noted too, as is the case in Figure 5. The second possible di erentiation is the status of the axiomatization, as discussed in Section 2.2. There are 12 possible annotations for the citation:

21

%-------------------------------------------------------------------------% File : GRP039-7 : TPTP v1.2.1. Bugfixed v1.0.1. % Domain : Group Theory (Subgroups) % Problem : Subgroups of index 2 are normal % Version : McCharen, et al., 1976] (equality) axioms : Augmented. % English : If O is a subgroup of G and there are exactly 2 cosets % in G/O, then O is normal that is, for all x in G and % y in O, x*y*inverse(x) is back in O]. % Refs % % % Source % Names % Status % Rating % Syntax % % % % % % : McCharen J.D., Overbeek R.A., Wos L.A. (1976), Problems and Experiments for and with Automated Theorem Proving Programs IEEE Transactions on Computers C-25(8), 773-782. : McCharen, et al., 1976] : GP2 McCharen, et al., 1976] : unsatisfiable : 0.89 v2.0.0 : Number of clauses Number of literals Maximal clause size Number of predicates Number of functors Number of variables Maximal term depth

: : : : : : :

25 43 4 2 8 38 3

( ( ( ( ( ( (

2 28 1 0 5 0 1

non-Horn; 13 unit; 12 RR) equality) average) propositional; 1-2 arity) constant; 0-2 arity) singleton) average)

% Comments : Used to define a subgroup of index two is a theorem which % says that {for all x, for all y, there exists a z such that % ... (some lines removed here for brevity) % Bugfixes : v1.0.1 - Duplicate axioms multiply_inverse_left and % multiply_inverse_right removed. %--------------------------------------------------------------------------

Figure 5: Example of a CNF problem le header (GRP039-7.p).

<empty>. Indicates that the axiomatization is standard, i.e., it is complete and has had no lemmas added (it may be redundant). Special. Indicates that the axiomatization does not capture any established theory. Incomplete. Indicates that the axiomatization is incomplete. Reduced > Complete. Indicates that a existing standard axiomatization has had axioms removed, and the result is complete. The existing axiomatization is necessarily redundant. Reduced > Incomplete. Indicates that a existing standard axiomatization has had axioms removed, and the result is non-standard due to incompleteness. Augmented. Indicates that a existing standard axiomatization has had lemmas added, and the result is non-standard due to redundancy. Reduced & Augmented > Complete. Indicates that a existing standard axiomatization has had axioms removed and lemmas added, and the result is complete. Reduced & Augmented > Incomplete. Indicates that a existing standard axiomatization has had axioms removed and lemmas added, and the result is non-standard due to incompleteness.

22

Incomplete > Reduced > Incomplete.

Indicates that an existing incomplete axiomatization has had axioms removed, and the result is non-standard due to incompleteness. Incomplete > Augmented > Complete. Indicates that an existing incomplete axiomatization has had axioms added, and the result is complete. Incomplete > Augmented > Incomplete. Indicates that an existing incomplete axiomatization has had lemmas added, and the result is non-standard due to incompleteness. Incomplete > Reduced & Augmented > Complete. Indicates that an existing incomplete axiomatization has had axioms removed and lemmas added, and the result is complete. Incomplete > Reduced & Augmented > Incomplete. Indicates that an existing incomplete axiomatization has had axioms removed and lemmas added, and the result is non-standard due to incompleteness.

In the problem of Figure 5, an existing standard axiomatization has been Augmented, and has become non-standard due to redundancy. The third possible di erentiation between problem versions is in the theorem formulation. Variations in the theorem formulation are noted in a Theorem formulation entry, e.g.,

% Version % :

McCharen, et al., 1976] (equality) axioms. Theorem formulation : Explicit formulation of the commutator.

description in the %

The %

English

eld. This eld provides a full description of the problem, if the one-line

Problem

eld is too terse.

The %

Refs eld. This eld provides a list of references in which the problem has been presented. Other relevant references are also listed.

The % Source eld. The problems in the TPTP have been (physically) obtained from a variety of sources, both hardcopy and electronic. In this eld the source of the problem is acknowledged, usually as a citation. If the problem was sourced from an existing problem collection then the collection name is given in ] brackets. The problem collections used thus far are:

ANL OTTER Quaife ROO SPRFN TPTP SETHEO - the Argonne National Laboratory library ANL], - the collection distributed with the Otter ATP system McC90, McC94] - Art Quaife's collection of set theory (based) problems Qua92c] - the problems used to test the ROO ATP system LM92] - the collection distributed with the SPRFN ATP system SPR], - the problem rst ever appeared in the TPTP SS96], - the collection used to test the SETHEO ATP system LSBB92].

McCharen, et al., 1976].

The problem of Figure 5 was taken from

The % Names eld. Problems which have appeared in other problem collections or the literature, often have names which are known in the ATP community. This eld lists all such names known to us for the problem, along with the source of the name. If the source

23

is an existing problem collection then the collection name is cited, as in the % Source eld. If the source of a name is a paper then a citation is given. If a problem is not given a name in a paper then \-" is used as the known name and a citation is given. Problems which rst appeared in the TPTP have source TPTP, and no other name. In generator les all known names for instances of the abstract problem are listed, with the instance size given before the source. A reverse index, from known names to TPTP names, is distributed with the TPTP (see Section 2.6). The problem of Figure 5 is called GP2 in McCharen, et al., 1976].

Status This eld gives the ATP status of the problem. For CNF problems it is one of tautology (all interpretations are models of the clauses), satisfiable (some, but not all, interpretations are models of the clauses), unsatisfiable (no interpretations are models of the clauses), unknown (the status of the clauses is unknown, but the abstract problem has been solved), or open (the abstract problem has not been solved). For FOF problems it is one of unsatisfiable (no model of the axioms and hypotheses is also a model of the conjecture), satisfiable (some, but not all, models of the axioms and hypotheses are models of the conjecture), theorem (all models of the axioms and hypotheses

The %

eld.

are models of the conjecture, including the case where the axioms and hypotheses have no models), unknown (the status of the formulae is unknown, but the abstract problem has been solved), or open (the abstract problem has not been solved). In Figure 5, the status is unsatisfiable.

state-of-the-art ATP systems. The rating is a real number in the range 0.0 to 1.0, where 0.0 means that all state-of-the-art ATP systems can solve the problem (i.e., the problem is easy), and 1.0 means no state-of-the-art ATP systems can solve the problem (i.e., the problem is hard). The rating is followed by a TPTP release number, indicating in which release the rating was assigned. If no rating has been assigned, a ? is given. In Figure 5, the rating is 0.89, assigned in release v2.0.0.

The %

Rating

eld. This eld gives the di culty of the problem, measured relative to

The %

Syntax eld. This eld lists various syntactic measures of the problem's clauses. The measures for CNF problems are: the number of clauses, the number of non-Horn clauses, the number of unit clauses, the number of range restricted clauses, the number if literals, the number of equality literals, the maximal and average clause size (measured by number of literals), the number of distinct predicate symbols, the number of distinct propositional symbols, the minimal and maximal predicate symbol arites, the number of distinct function symbols, the number of distinct constants, the minimal and maximal functor arites, the number of distinct variables, the number of singleton variables (variables that appear only once in a clause), and the maximal and average term depth (with constants and variables having depth 1). The measures for FOF problems are: the number of formulae, the number if unit formulae, the number of atoms, the number of equality atoms, the maximal and average formula depth, the number of connectives, the numbers of each type of connective, the number of distinct propositional symbols, the minimal and maximal predicate symbol arites, the number of distinct function symbols, the number of distinct constants, the minimal and maximal functor arites, the number of distinct variables, the number of singleton variables, the numbers of universally and existentially quanti ed variables, and the maximal and average term depth. See Tables 4-7

24

for a summary of this information over the entire TPTP.

The % The

Comments eld. This eld contains free format comments about the problem, e.g., the signi cance of the problem, or the reason for creating the problem. If the problem was created using the tptp2X utility (see Section 3.1) then the tptp2X parameters are given. % Bugfixes

clauses of the problem. Each entry gives the release number in which the bug x was done, and attempts to pinpoint the bug x accurately. In the problem of Figure 5, a bug x was made in release v1.0.1, by removing the duplicate multiply inverse left and multiply inverse right clauses.

eld. This eld describes any bug xes that have been done to the

2.5.2 The Include Section

The include section contains include instructions for TPTP axiom les. An example of an include section is shown in Figure 6, extracted from the problem le GRP039-7.p.

%-------------------------------------------------------------------------%----Include the axioms of equality include('Axioms/EQU001-0.ax'). %----Include the axioms for group theory in equality form include('Axioms/GRP004-0.ax'). %----Include the subgroup axioms in equality formulation include('Axioms/GRP004-1.ax'). %--------------------------------------------------------------------------

Figure 6: Example of a problem le include section (GRP039-7.p). Each of the include instructions indicates that the formulae in the named axiom le should be included at that point. Axiom les are presented in the same format as problem les, and include instructions may also appear in axiom les. If required, full versions of TPTP problems (without include instructions) can be created by using the tptp2X utility (see Section 3.1).

2.5.3 The Formulae Section for FOF Problems

The atoms that appear in a formula are presented in the form of Prolog terms. The connectives used to build non-atomic formulae are pre x ~ for negation; in x | for disjunction, in x & for conjunction, in x <=> for equivalence, in x => for implication, in x <= for reverse implication, in x <~> for non-equivalence (XOR), in x ~| for negated disjunction (NOR), and in x ~& for negated conjunction (NAND). Negation has higher precedence than the binary connectives, but no precedence between binary connectives is assumed; brackets are used to ensure the correct association. The universal quanti er is ! and the existential quanti er is ?. Quanti ed formulae are written in the form <Quanti er> <Variables>] : <Formula>. FOF formulae can be read as Prolog terms using appropriate operator de nitions. 25

Each formula has a name, in the form of a Prolog atom. Each formula also has a type, one of axiom, hypothesis, or conjecture. The name, type, and formula are bundled as the three arguments of a Prolog fact, whose predicate symbol is input formula. These facts are in the formulae section of the problem le. An example of a formula section, extracted from the problem le GRP194+1.p, is shown in Figure 7.

%-------------------------------------------------------------------------input_formula(phi_substitution_1,axiom,( ! A,B] : ( equal(A,B) => equal(phi(A),phi(B)) ) )). %----Definition of a homomorphism input_formula(homomorphism1,axiom,( ! X] : ( group_member(X,f) => group_member(phi(X),h) ) )). <some formulae omitted> %----Definition of left zero input_formula(left_zero,axiom,( ! G,X] : ( left_zero(G,X) <=> ( group_member(X,G) & ! Y] : ( group_member(Y,G) => equal(multiply(G,X,Y),X) ) ) ) %----The conjecture input_formula(left_zero_for_f,hypothesis,( left_zero(f,f_left_zero) )). input_formula(prove_left_zero_h,conjecture,( left_zero(h,phi(f_left_zero)) )). %--------------------------------------------------------------------------

)).

Figure 7: Example of a FOF problem le formulae section (GRP194+1.p).

2.5.4 The Clauses Section for CNF Problems

The literals that make up a clause are presented as a Prolog list of terms (i.e., in ]). Each literal is a term whose functor is either ++ or --, indicating a positive or negative literal, respectively. The atom of the literal is the single argument of the sign, in the form of a Prolog term. Thus predicate symbols and functors start with lower case alphanumeric, and variables start with upper case alphabetic. Variables may not start with an . All symbols contain only alphanumerics and . If a symbol starts with a numeric, it contains only numerics (i.e., it is a number). The signs ++ and -- are assumed to be de ned as pre x operators in Prolog. 26

Each clause has a name, in the form of a Prolog atom. Each clause also has a type, one of axiom, hypothesis, or conjecture. The hypothesis and conjecture clauses are those that are derived from the negation of the conjecture to be proved. These clauses are only of type hypothesis if they can clearly be determined as such; otherwise they are of type conjecture. The name, type, and literal list of each clause are bundled as the three arguments of a Prolog fact, whose predicate symbol is input clause. These facts are in the clauses section of the problem le. An example of a clause section, extracted from the problem le GRP039-7.p, is shown in Figure 8.

%-------------------------------------------------------------------------%----Redundant two axioms input_clause(right_identity,axiom, ++equal(multiply(X,identity),X)]). input_clause(right_inverse,axiom, ++equal(multiply(X,inverse(X)),identity)]). <some clauses omitted> %----Denial of theorem input_clause(b_in_O2,hypothesis, ++subgroup_member(b)]). input_clause(b_times_a_inverse_is_c,hypothesis, ++equal(multiply(b,inverse(a)),c)]). input_clause(a_times_c_is_d,hypothesis, ++equal(multiply(a,c),d)]). input_clause(prove_d_in_O2,conjecture, --subgroup_member(d)]). %--------------------------------------------------------------------------

Figure 8: Example of a CNF problem le clause section (GRP039-7.p).

2.6 Physical Organization

The TPTP is physically organized into six subdirectories, as follows:

Axioms

- The axiom les directory. Problems - The problem les directory with subdirectories for each domain. The domain name abbreviations, as described in Section 2.1, are used as subdirectory names. The subdirectories contain the problem les. Generators - The generator les directory. Documents - A directory containing documents that relate to the TPTP : 27

- A list of the axiomatizations in the TPTP, giving their names, number of FOF and CNF specializations, and one-line descriptions. { GeneratorList - A list of the generic problems in the TPTP, giving their names, number of FOF and CNF versions, and one-line descriptions. For each version the constraints that determine the permissible sizes and the TPTP size are given. { ProblemList - A list of all the abstract problems in the TPTP, giving their names, number of FOF and CNF versions, and one-line descriptions. { FOFProblemStatistics and CNFProblemStatistics - Lists of the FOF and CNF problems in the TPTP, giving information about the axiomatization used (S = standard, I = incomplete, A = augmented, { = special), the % Status value (T = theorem (FOF) or tautology (CNF), S = satis able, U = unsatis able, O = open, ? = unknown), and the % Syntax eld values. { FOFProblemStatistics.rm eq and CNFProblemStatistics.rm eq - Lists of the FOF and CNF problems in the TPTP, giving the information as in the FOFProblemStatistics and CNFProblemStatistics les, but after removing all equality axioms from the problem (done using tptp2X, see Section 3.1). { ReadMe - General information about the TPTP. { ReverseIndex - An index from existing known names for problems to their TPTP le names. { FOFSynopsis and CNFSynopsis - Statistics on the FOF and CNF parts of the TPTP, as given in Tables 2-8, and a chart showing the structure of the TPTP problem domains, as given in Figure 1. { OverallSynopsis - Statistics on the overall TPTP, as given in Tables 1 and 8, and a chart showing the structure of the TPTP problem domains, as given in Figure 1. { Template - A template for submitting new TPTP problems. { Users - A list of registered TPTP users. Registered users receive noti cation of TPTP patches, and other information relevant to the TPTP. If you would like to have your name added to or removed from this list, please let us know. Our addresses are given in Section 4.3. The les in the Documents directory contain comprehensive online information about the TPTP. They summarize much of the information contained in this report, in speci c les. Their format provides quick access to the data, using standard system tools (e.g., grep, awk). TPTP2X - The directory containing the tptp2X utility, described in Section 3.1. Scripts - A directory containing C shell scripts that may be used with the TPTP, as described in Section 3.2.

AxiomList

{ {

History - A history of the changes made to the TPTP up to the current release.

28

3 Utility Programs and Scripts

3.1 The tptp2X Utility

The tptp2X utility is a multi-functional utility for reformatting, transforming, and generating TPTP problem les. In particular, it Converts from the TPTP format to formats used by existing ATP systems. Applies various transformations to TPTP problems. Controls the generation of TPTP problem les from TPTP generator les. The tptp2X utility is written in Prolog, and should run on most Prolog systems2 . There is some code that is speci c to the BinProlog, SICStus 2.1, Quintus, and Eclipse Prolog dialects. Before using tptp2X, it is necessary to install the code for the dialect of Prolog that is to be used. This and other installation issues are described next.

3.1.1 Installation

The tptp2X utility consists of the following les:

tptp2X - A tcsh script for running the tptp2X utility. tptp2X install - A csh script for installing the tptp2X utility. tptp2X.config - Con guration le with site speci c information. tptp2X.main - The main source code le of the tptp2X utility. tptp2X.read - Procedures for reading TPTP problem les. tptp2X.generate - Procedures for using TPTP generator les. tptp2X.syntax - Procedures for extracting syntactic measures from les. transform.<TRAN> - Procedures for doing <TRAN> transformations format.<ATP>

problems.

on TPTP

- Procedures for outputing formulae in <ATP> format.

tptp2X.config and tptp2X.main.

Installation of the tptp2X utility requires simple changes in the tptp2X script and the les These changes can be made by running tptp2X install, which will prompt for required information. Otherwise, to install tptp2X by hand, the following must be attended to: In the tptp2X script le: TPTPDirectory must be set to the absolute path name of the TPTP directory. PrologInterpreter must be set to the absolute path name of the Prolog interpreter. PrologArguments must be set to any command line arguments for the Prolog interpreter. The Gawk variable must be set to the absolute path name of gawk or awk. In the tptp2X.config le: The appropriate facts for the desired Prolog dialect must be uncommented.

2 In particular, the tptp2X code will run on BinProlog 5.00. BinProlog is written by Paul Tarau of the University of Moncton (Canada), and is freely available by anonymous ftp, from clement.info.umoncton.ca:BinProlog.

29

The absolute path name of the TPTP directory must be set in the tptp directory/1 fact. In the tptp2X.main le: If your Prolog interpreter does not support compile/1 for loading source code, the compile/1 directives must be changed to something appropriate, e.g., ].

3.1.2 Using tptp2X

The most convenient way of using the tptp2X utility is through the tptp2X script. The use of this script is:

tptp2X -h] -q<Level>] -i] -s<Size>] -t<Transform>] -f<Format>] -d<Directory>] <TPTPFiles>

The -h ag speci es that usage information should be output. The -q<Level> ag speci es the level of quietness at which the script should operate. There are three quietness levels; 0 is verbose mode, 1 suppresses informational output from the Prolog interpreter, and 2 suppresses all informational output except lines showing what les are produced. The default quietness level is 1. The -i ag speci es that the script should enter interactive mode after processing all other command line parameters. Interactive mode is described below. The other command line parameter values are:

-s<Size>

: This speci es the required sizes when generating problems. <Size> is either an integer, a <Low>..<High> integer size range, or a : separated list of <Sizes>. { An integer directly speci es the required problem size. { Each integer in a size range is used to generate a separate set of formulae. { A : separated string of <Sizes> is used for generators that require multiple parameters, one <Size> for each size parameter required. For example, -s3..5:2 means the three sizes 3:2, 4:2, and 5:2. -s<Size> is ignored for problem (.p) les. -t<Transform> : Speci es transformations to be applied to the formulae. <Transform> is either a single transformation, a + separated string of transformations, or a comma separated list of <Transform>s. { A single transformation is applied directly to the formulae. { The transformations in a + separated string are applied to the formulae serially. { Each <Transform> in a comma separated list of <Transform>s is used to create a separate set of transformed formulae. The transformations are: { clausify:<Algorithm>, to transform FOF problems to CNF problems. The <Algorithm> is one of: bundy, to use the algorithm presented in Bun83], 30

{ { { { { { { { { {

{

to use the algorithm used in Otter McC94], quaife, to use Art Quaife's algorithm Qua90], tptp, to use an algorithm combining features of the otter and quaife algorithms. Details of these algorithms can found in SM96]. Note that alone these transformation do no simpli cation of the resultant clause set; see the next two transformations for this. simplify, to simplify a set of clauses. Details of the simpli cations performed can be found in SM96]. cnf:<Algorithm>, to do clausify:<Algorithm> followed by simplify. Details of the performance of these transformations can be found in SM96]. Generally cnf:otter and cnf:bundy produce clause sets with lower symbol counts than the other two. lr, to reverse the literal ordering in the clauses of CNF problems. cr, to reverse the clause ordering in CNF problems. clr, to do both clausal reversals. fr, to reverse the formula ordering in FOF problems. random, to randomly reorder the clauses and literals in CNF problems, or to randomly reorder the formulae in FOF problems. The rearrangement of formulae, clauses, and literals in a problem facilitates testing the sensitivity of an ATP system to the order of presentation. er, to reverse the arguments of all clauses in unit equality CNF problems. ran er, to reverse the arguments of randomly selected clauses in unit equality CNF problems. rm equality:<Remove>, to remove equality axioms. <Remove> is a string that indicates which equality axioms to remove. The characters that can be in the string are: r, to remove re exivity, s, to remove symmetry, t, to remove transitivity, f, to remove function substitution, p, to remove predicate substitution. For example, -t rm equality:stfp would indicate to remove symmetry, transitivity, function substitution, and predicate substitution. This transformation works only if the equality axiomatization is complete (i.e., including the axioms of re exivity, symmetry, transitivity, function substitution for all functors, and predicate substitution for all predicate symbols), using equal/2 as the equality predicate. (All TPTP problems containing the equal/2 predicate contain a complete equality axiomatization; see Section 2.2.) add equality, to add missing equality axioms. If the problem contains the equal/2 predicate, then a check is made to see if the equality axiomatization is complete. If not, the missing equality axioms are added to the problem. 31

otter,

to convert CNF problems to a pure equality representation. Every non-equality literal is converted to an equality literal (using the equal/2 predicate) with the same sign. The arguments of the new equality literal are the atom of the non-equality literal and the constant true. { magic, to do Mark Stickel's magic set transformation Sti94] to CNF problems. { shorten, to replace all the symbols in the problem by short, meaningless symbols. This is useful if you are only interested in the syntax of the problem, and do not want to read through the long, meaningful symbols that are often used in TPTP problems. Note that equal/2 is not shortened. { none, to do nothing (same as omitting the -t parameter, but required for advanced use; see Section 3.1.5). The default <Transform> is none. -f<Format> : Speci es the format in which the output is to be written. The available output formats are: { clin s, to convert CNF problems to the CLIN-S format CP94, Chu94], { dfg, to convert CNF problems to the DFG format HKW96], { dimacs, to convert propositional CNF problems to the DIMACS format DIM], { ilf, to convert CNF problems to the ILF format DGH+95], { kif, to convert CNF problems to the KIF format GF92], { leantap, to convert CNF problems to the leanTAP format BP95], { tap, to convert CNF problems to the 3TAP format HBG94], { meteor, to convert CNF problems to the METEOR format Ast94], { mgtp, to convert CNF problems to the MGTP format FHKF92], { oscar, to convert FOF problems to the OSCAR format Pol90], { otter:<SoS>:'<Otter options>', to convert FOF and CNF problems to the Otter .in format McC94]. <SoS> speci es the Set-of-Support to use. It can be one of: conjecture, to use the formulae whose type is conjecture, hypothesis, to use the formulae whose type is hypothesis or conjecture, to use the positive clauses, to use the negative clauses, unit, to use the unit clauses, all, to use all formulae, none, to use no formulae (needed fo Otter's auto mode). '<Otter options>' is a quoted (to avoid UNIX shell errors), comma separated list of Otter options, which will be output before the formula lists. See the Otter Reference Manual and Guide McC94] for details of the available options. For example, -f otter:none:'set(auto),assign(max seconds,5)' would congure Otter to use its auto mode with a time limit of 5 seconds. As the auto

negative, positive,

{

to equality,

32

mode is commonly used with Otter, the tptp2X script allows the abbreviation -f otter to specify -f otter:none:'set(auto)'. If no -t parameter is speci ed then -f otter also sets -t equality:stfp. { pttp, to convert CNF problems to the PTTP format Sti84]; { setheo:<Style>,to convert CNF problems to the SETHEO .lop format STvdK90]. <Style> speci es the style of SETHEO clauses to write. It can be one of: sign, to write the atoms of the negative and positive literals of each clause in the antecendent and consequent of an implication, respectively; type In the type style, if there are no negative axiom or hypothesis clauses, then the sign style is used. Otherwise in all negative axiom and hypothesis clauses the rst literal is negated to form the consequent of an implication, with the remaining literals' atoms being written as the antecedent. Further, in all conjecture clauses all positive literals are negated so that all literals are written in the antecedent of an implication. The default style is sign, i.e., the abbreviation -fsetheo means -fsetheo:sign. { sprfn, to convert CNF problems to the SPRFN format Pla88]; { tptp, to convert FOF and CNF problems to the TPTP format, substituting include instructions with the actual formulae. The default <Format> is tptp. -d<Directory> : Speci es the top level directory below which the output les are to be placed. If the <Directory> value is -, then all output les are written to standard output. Otherwise the output les associated with an input le are placed in a subdirectory below the <Directory>, named according to the domain (the rst 3 characters) of the input le. The default <Directory> is a subdirectory below the TPTP Problems directory, named according to the <Format>. <TPTPFiles> : Lists the input les which are to be processed. As a shortcut, the three letter domain names can be given, which processes all problems in those domains. If speci c les names are not absolute, then tptp2X looks in the current working directory, the Generators directory, the Problems directory, and the domain directories, for the le. If the le name - is speci ed then input is taken from standard input and all output is written to standard output (overriding any <Directory> speci cation). The default <TPTPFiles> are all TPTP problem les. Hint: If your command shell complains about too many arguments as a result of expanding the <TPTPFiles> argument to a too large number of les, e.g., ~/TPTP/Problems/S*/*.p, place the <TPTPFiles> argument in 'single quotes', and tptp2X will do the expansion internally. A common rst use of tptp2X is to convert TPTP problems to another format. To convert all TPTP problems to another format, the use is tptp2X -f<Format>, e.g., tptp2X -fotter. To limit the conversion to one or more domains, the domain names are speci ed after the <Format>, e.g., tptp2X -fleantap ALG GRP LDA. If you are a new TPTP user, these are probably the uses that you want to start with. 33

3.1.3 The tptp2X Output Files

The output les produced by tptp2X are named according to the TPTP le name and the options used. The name of the TPTP problem (the input le name without the .p or .g) forms the basis of the output le names. For les created from TPTP generators, the size parameters are appended to the base name, separated from the base name by a \.". Then, for each transformation applied a su x is appended. The su xes for the transformations are: Transformation clausify:<Algorithm> simplify cnf:<Algorithm> lr cr clr fr random er ran er rm equality:<Remove> add equality to equality magic shorten none Su x +cls <Algorithm> +simp +cnf <Algorithm> +lr +cr +clr +fr +ran +er +ran er +rm eq <Remove> +eq +2eq +nhms +short

Finally an extension to indicate the output format is appended to the le name. The su xes for the output formats are: Format clin-s dfg dimacs ilf kif leanTAP tap meteor mgtp oscar otter pttp setheo sprfn tptp Extension .clin s .dfg .dimacs .ilf .kif .leantap .3tap .me .mgtp .oscar .in .pttp .lop .sprfn .tptp

To record how a tptp2X output le has been formed, the tptp2X parameters are listed as an entry in the % Comments eld of the output le. 34

Example

~/TPTP/TPTP2X> tptp2X -tlr,cr,clr -fpttp ../Problems/ALG/ALG001-1.p --------------------------------------------------------------------TPTP2X directory = /home/geoff/TPTP/TPTP2X TPTP directory = /home/geoff/TPTP Prolog interpreter = /usr/local/bin/sicstus Files to convert = ../Problems/ALG/ALG001-1.p Size = Transformation = lr,cr,clr Format to convert to = pttp Output directory = /home/geoff/TPTP/Problems/pttp --------------------------------------------------------------------Made the directory /home/geoff/TPTP/Problems/pttp/ALG ALG001-1 -> /home/geoff/TPTP/Problems/pttp/ALG/ALG001-1+lr.pttp ALG001-1 -> /home/geoff/TPTP/Problems/pttp/ALG/ALG001-1+cr.pttp ALG001-1 -> /home/geoff/TPTP/Problems/pttp/ALG/ALG001-1+clr.pttp ~/TPTP/TPTP2X>

This run applies three separate transformations to the problem ALG001-1. The transformations are literal order reversal, clause order reversal, and reversal of both literal and clause order. The transformed problems are output in pttp format, in the directory pttp/ALG below the TPTP Problems directory. The le names are ALG001-1+lr.pttp, ALG001-1+cr.pttp, and ALG001-1+clr.pttp.

Example

~/TPTP/TPTP2X> tptp2X -q2 -s3..5 -fotter -d~geoff/tmp ../Generators/SYN001-1.g SYN001-1 -> /home/geoff/tmp/SYN/SYN001-1.003+eq_stfp.in SYN001-1 -> /home/geoff/tmp/SYN/SYN001-1.004+eq_stfp.in SYN001-1 -> /home/geoff/tmp/SYN/SYN001-1.005+eq_stfp.in ~/TPTP/TPTP2X>

This run generates three sizes of the generic problem SYN001-1. The sizes are 3, 4, and 5. The output les are formatted for Otter, to use its auto mode. The les are placed in ~geoff/tmp/SYN, and are named SYN001-1.003.lop, SYN001-1.004.lop, and SYN001-1.005.lop. The quietness level is set to 2, thus suppressing all informational output except the lines showing what les are produced.

Example

~/TPTP/TPTP2X> tptp2X -q2 -tmagic+shorten - < ~geoff/TPTP/Problems/GRP/GRP001-1.p %-------------------------------------------------------------------------% File : GRP001=SqrComm-1 : TPTP v1.1.3. Released v1.0.0. % Domain : Group Theory % Problem : X^2 = identity => commutativity <Lots of output> input_clause(clause_41,theorem, --p2(c8,c7,c9)]). %-------------------------------------------------------------------------~/TPTP/TPTP2X>

This run uses the tptp2X script as a lter, to apply the non-Horn magic set transformation and then the symbol shortening transformation to GRP001-1.p. GRP001-1.p is fed in from 35

standard input, and the output is written to standard output. The quietness level is set to 2, and as the output is to standard output, all informational output is suppressed.

3.1.4 The tptp2X Interactive Mode

If the -i ag is set, the tptp2X script enters interactive mode after processing all other command line parameters. In interactive mode the user can change the value of any of the command line parameters. The user is prompted for the <TPTPFiles>, the <Size>, the <Transform>, the <Format>, and the <Directory>. In each prompt the current value is given. The user may respond by specifying a new value or by entering <cr> to accept the current value. The prompt-respond loop continues for each parameter until the user accepts the current value for the parameter.

Example

~/TPTP/TPTP2X> tptp2X -q0 -d~geoff/tmp -i ---- Interactive mode ----------------------------------------------Files to convert Problems/*/*.p] : ../Problems/GRP/GRP001-1.p Files to convert ../Problems/GRP/GRP001-1.p] : Size ] : Transformation none] : lr+equality:stfp Transformation lr+equality:stfp] : Format to convert to tptp] : setheo Format to convert to setheo] : Output directory /home/geoff/tmp] : ---- End of Interactive mode -----------------------------------------------------------------------------------------------------------TPTP2X directory = /home/geoff/TPTP/TPTP2X TPTP directory = /home/geoff/TPTP Prolog interpreter = /usr/local/bin/sicstus Files to convert = ../Problems/GRP/GRP001-1.p Size = Transformation = lr+equality:stfp Format to convert to = setheo:sign Output directory = /home/geoff/tmp --------------------------------------------------------------------Made the directory /home/geoff/tmp/GRP SICStus 2.1 #9: Thu Apr 21 09:39:25 +1000 1994 {compiling /home/2/geoff/TPTP/TPTP2X/tptp2X.main...} <Lots of informational output> {/home/2/geoff/TPTP/TPTP2X/tptp2X.main compiled, 19906 msec 248400 bytes} yes yes GRP001-1 -> /home/geoff/tmp/GRP/GRP001-1+lr+eq_stfp.lop yes ~/TPTP/TPTP2X>

This run converts the problem GRP001-1 to a SETHEO format le. The literals are reversed and all equality clauses except re exivity are removed. The top level output 36

directory is speci ed as ~geoff/tmp, below which the subdirectory GRP is made. The output le is named GRP001-1+lr+eq stfp.lop. Verbose mode is used, so all informational output is given. The following subsections are only of interest to real Prolog users. If you do not want to use Prolog directly, skip to the next section.

3.1.5 Running tptp2X from within Prolog

The tptp2X utility may also be run from within the Prolog interpreter. The tptp2X.main le has to be loaded, and the entry point is then tptp2X/5, in the form: ?-tptp2X(<TPTPFile>,<Size>,<Transform>,<Format>,<Directory>). The parameters are similar to the tptp2X script command line parameters. A summary, highlighting di erences with \(!)", is given here. See Section 3.1.2 for parameter options.

<TPTPFile> is the name of a single TPTP le. If the le name is not absolute, then it is considered to be relative to the directory speci ed in the tptp directory/1 fact in the tptp2X.config le (!). If the le name is user (!), then input is taken from standard input. <Size> is either an integer, a : separated string of <Size>s, a <Low>..<High> integer size range, or a Prolog list of <Size>s (!). Each <Size> in a Prolog list of <Size>s is used in all possible ways to generate separate sets of formulae. <Transform> is either a single transformation speci er, a + separated string of <Transform>s (!), or a Prolog list (!) of <Transform>s. <Format> is an output format or a Prolog list (!) of output formats. An output le is written for each output format speci ed. For the otter format, the syntax is otter:<SoS>: <Otter options>] (!), i.e., the Otter options form a Prolog list. <Directory> speci es the directory in which the output les are to be placed. If the <Directory> is user (!) then output is sent to standard output.

37

Example

~/TPTP/TPTP2X> sicstus SICStus 2.1 #9: Thu Apr 21 09:39:25 +1000 1994 | ?- 'tptp2X.main']. {consulting /home/2/geoff/TPTP/TPTP2X/tptp2X.main...} <Lots of informational output> {/home/geoff/TPTP/TPTP2X/tptp2X.main consulted, 19158 msec 256800 bytes} yes | ?- tptp2X('Generators/SYN010-1.g',3: 2,4], lr,cr]+magic,kif,'.'). {compiling /home/geoff/TPTP/Generators/SYN010-1.g...} {/home/geoff/TPTP/Generators/SYN010-1.g compiled, 246 msec 2240 bytes} SYN010-1 -> ./SYN010-1.003:002+lr+nhms.kif SYN010-1 -> ./SYN010-1.003:002+cr+nhms.kif SYN010-1 -> ./SYN010-1.003:004+lr+nhms.kif SYN010-1 -> ./SYN010-1.003:004+cr+nhms.kif yes | ?- ^D ~/TPTP/TPTP2X>

This run generates two sizes of the generic problem SYN010-1, and does two transformation sequences on each of the two sets of clauses, to produce four output les. The sizes are 3:2 and 3:4. The rst transformation sequence is literal order reversal followed by the nonHorn magic set transformation, and the second transformation sequence is clause order reversal followed by the non-Horn magic set transformation. The les are output in KIF format in the current directory. The le names are SYN010-1.003:002+lr+nhms.kif, SYN010-1.003:002+cr+nhms.kif, SYN010-1.003:004+lr+nhms.kif, and SYN010-1.003:004+cr+nhms.kif. Note that the TPTP le name is quoted in the query, to form a Prolog atom.

3.1.6 Writing your own Transformations and Output Formats

The transformations and output formating are implemented in Prolog, in the les and format.<ATP>, respectively. It is simple to add new transformations and output formats to the tptp2X utility, by creating new transformation and format les. New les should follow the structure of the existing les. Typically, a new le can be created by modifying a copy of one of the existing les. The entry point in a transformation le is <Transform>/6, where <Transform> is the principle symbol of the transformation speci cation. The rst three arguments are inputs: a list of the problem's formulae, the variable dictionary (a bit complicated), and the transformation speci cation. The next three arguments are outputs: the transformed formulae, the transformed variable dictionary (typically the same as the input dictionary), and the transformation su x. As well as the <Transform>/6 entry point, a <Transform> file information/2 fact must be provided. The two arguments of the <Transform> file information/2 fact are the atom transform and a description of the possible transformation speci cations (as used in the third argument of <Transform>/6). See the existing transform.<TRAN> les for examples. The entry point in a format le is <Format>/3, where <Format> is the principle symbol of the output format speci cation. The three arguments are inputs: the format speci cation,

transform.<TRAN>

38

a list of the problem's formulae, and the le header information. (It is not necessary to output a le header here; this information is available only for producing supplementary documentation.) As well as the <Format>/3 entry point, a <Format> format information/2 fact and a <Format> file information/2 fact must be provided. The two arguments of the <Format> format information/2 fact are a character that can be used to start a comment in the output le and the format extension, both as Prolog atoms. The two arguments of the <Format> file information/2 fact are the atom format and a description of the possible format speci cations (as used in the rst argument of <Format>/3). See the existing format.<ATP> les for examples. New transformation and format les must be compiled in with the other tptp2X les. This is done by adding a compile query in the tptp2X.main le, alongside the queries that compile in the existing les. If you are in doubt, please contact Geo Sutcli e for help.

3.1.7 Writing your own Problem Generators

The TPTP generators are implemented in Prolog. It is simple to write new generators. New les should follow the structure of the existing les. The entry point in a generator le is <Problem name>/3, where <Problem name> is the le name without the .g su x. The rst argument is an input: the size parameter for generation. The second and third arguments are outputs: the formulae generated and the status of the formulae. The formulae must be a Prolog list of formulae in TPTP format. A <Problem name> file information/3 fact must also be provided. The three arguments of the fact are the atom generator, a description of the possible size parameters (as used in the rst argument of <Problem name>/3), and the TPTP size for this problem (this is hard to determine!). See the existing generator les for examples. If you are in doubt, please contact Geo Sutcli e for help.

3.2 The tptp1T Script

The tptp1T script selects lines from either the CNFProblemStatistics le or the FOFProblemStatistics le, by problem characteristics. The tptp1T script is written perl v5.

3.2.1 Installation

Installation of the tptp1T utility requires simple changes in the tptp1T script. These changes can be made by running tptp1T install, which will prompt for required information. Otherwise, to install tptp1T by hand, in the tptp1T script le $TPTPDirectory must be set to the absolute path name of the TPTP directory.

3.2.2 Using tptp1T

The use of this script is:

tptp1T CNF|FOF

The CNF or FOF argument indicates which statistics le to select lines from. The optional -f <ProblemFile> argument speci es the name of a le containing TPTP problem names. 39

-f

<ProblemFile>] <Constraint> <Constraint>

...

tptp1T will select statistics <ProblemFile>, subject to

le lines for only those problems whose names appear in the the <Constraint>s. The problem names (without the .p extension) must appear one per line in the <ProblemFile>, and lines that start with # are ignored. The <Constraint>s specify required problem characteristics, all of which must be satis ed for the statistics le line to be selected. The possible <Constraint>s are: <Domain>, to select problems from only this domain. Standard, NonStandard, Incomplete, Augmented, or Special, to select problems with this axiomatization status (see Section 2.5.1). Rating <Minimum> <Maximum> to select problems whose % Rating is in the speci ed range. Theorem, Satisfiable, or Unsatisfiable to select FOF problems with this % Status. Unsatisfiable, Satisfiable, or Tautology to select CNF problems with this % Status. Open to select open problems. Propositional or NonPropositional to select propositional or non-propositional problems. Variables, NoVariables to select problems with or without variables. MinimalPredicateArity <Minimum> <Maximum> to select problems whose minimal predicate arity is in the speci ed range, and MaximalPredicateArity <Minimum> <Maximum> to select problems whose maximal predicate arity is in the speci ed range. NoEquality, SomeEquality, or PureEquality to select problems with no, some (but not purely), or purely equality atoms. AnyEquality selects problems with any equality atoms, i.e., the union of SomeEquality and PureEquality. Functions or NoFunctions to select problems have functions or have no functions (constants are considered to be functions of arity 0). MinimalFunctionArity <Minimum> <Maximum> to select problems whose minimal function arity is in the speci ed range, and MaximalFunctionArity <Minimum> <Maximum> to select problems whose maximal function arity is in the speci ed range. Horn or NonHorn to select CNF problems which are Horn or non-Horn. RangeRestricted or NonRangeRestricted to select CNF problems that are range restricted or not range restricted. AverageLiterals <Minimum> <Maximum> to select CNF problems in which the average number of literals per clause is in the speci ed range. UnitEquality or NonUnitEquality to select CNF problems that have only unit equality clauses or have some non-unit equality clauses. 40

4 You and the TPTP

4.1 Quick Installation Guide

This section explains how to obtain and install the TPTP, and how to syntax-convert the TPTP problems.

4.1.1 Obtaining the TPTP via FTP

The distribution consists of three les: ReadMe-v2.0.0 (9.0 kByte) contains an overview of the TPTP. TR-v2.0.0.ps.gz (0.1 MByte, 0.4 MByte unpacked) contains this version of the TPTP technical report. TPTP-v2.0.0.tar.gz (0.8 MByte, 20.1 MByte unpacked) contains the library (including a copy of the ReadMe-v2.0.0 le). There also might be a le called BuggedProblems-v2.0.0, containing a list of les that have been found to contain errors, in the current release (bugs that have been discovered after the release has been distributed). Ftp instructions for obtaining the TPTP from Australia or Germany:

prompt> cd <the directory where you want the TPTP to reside> prompt> ftp -i ftp.cs.jcu.edu.au # or: ftp -i 137.219.17.4 # or use alternatively ftp -i flop.informatik.tu-muenchen.de # or: ftp -i 131.159.8.35 Name (ftp.cs.jcu.edu.au:<your login-name>): ftp 331 Guest login ok, send your complete e-mail address as password. Password:<your full email address> ftp> cd pub/research/tptp-library # on ftp.cs.jcu.edu.au cd pub/tptp-library # on flop.informatik.tu-muenchen.de ftp> binary ftp> mget * ftp> quit

Or use the World Wide Web (WWW) with either of the following URLs :

http://www.cs.jcu.edu.au.yzcaijing.com/~tptp http://wwwjessen.informatik.tu-muenchen.de.yzcaijing.com/~tptp.

4.1.2 Installing the TPTP

prompt> gunzip -c TPTP-2.0.0.tar.gz | tar xvf prompt> TPTP-2.0.0/TPTP2X/tptp2X_install <... the script will then ask for required information> prompt> TPTP-2.0.0/Scripts/tptp1T_install <... the script will then ask for required information>

If you don't have any Prolog installed, you need to get one rst. BinProlog is freely available via anonymous ftp from clement.info.umoncton.ca:BinProlog. 41

4.1.3 Converting Problems to Other Syntax

prompt> TPTP-v2.0.0/TPTP2X/tptp2X <desired_syntax>

As <desired syntax>, choose any one of clin s, dfg, dimacs, ilf, kif, leantap, tap, meteor, mgtp, oscar, otter, pttp, setheo, sprfn, or tptp. Some of the formats cannot cope with certain types of problems, e.g., dimacs format is for only propositional CNF problems. The tptp format simply expands include directives (see Section 2.5) in problems, producing les in the TPTP Prolog-style syntax. tptp2X o ers MUCH more than this. See Section 3.1 for a detailed description of the utility, including information on how to produce output in your own syntax.

4.2 Important: Using the TPTP

By providing this library of ATP problems, and a speci cation of how these problems should be presented to ATP systems, it is our intention to place the testing, evaluation, and comparison of ATP systems onto a rm footing. For this reason, you should abide by the following conditions when using TPTP problems and presenting your results: The TPTP release number must be stated. Each problem must be referenced by its unambiguous syntactic name. No formulae may be changed, added, or removed without explicit notice (this holds also for removing equality axioms when built-in equality is provided by the prover). The formulae may not be reordered without explicit notice. If any reordering is done using the tptp2X utility, (see Section 3.1), the reordering must be explicitly noted. The header information in each problem may not be used by the ATP system without explicit notice. Any information that is given to the ATP system, other than that in the input formulas and input clauses, must be explicitly noted. All system switches and default settings must be recorded. Abiding by these rules will allow unambigous identi cation of the problem, the formulae, and further input to the ATP system. If you follow these rules, please make this clear in any presentation of your results, by an explicit statement. We propose that you state \These results were obtained in compliance with the guidelines for use of TPTP v2.0.0". By making this clear statement, ATP researchers are assured of your awareness of our guidelines. Conversely, it will become clear when the guidelines may have been ignored.

4.3 Please contact us if ...

Please contact one of us if: You nd any mistakes in the TPTP. You are able to provide further information for a TPTP problem. 42

You want to contribute a problem to the TPTP. Please use the problem template that comes with the distribution (in the Documents directory - see Section 2.6) and ll in header information as far as possible. Any unambiguous representation will do for the formulae. You have any suggestions for improving the TPTP library. Our contact addresses are: Geo Sutcli e - geo @cs.jcu.edu.au (FAX: +61 77 814029) Christian Suttner - suttner@informatik.tu-muenchen.de (FAX: +49 89 526502)

5 The Future

5.1 Current Activities

The collection of more FOF problems is continuing. A FOF axiomatization of set theory is being carefully built. Everybody is invited to submit problems in FOF syntax for inclusion. Please contact us for details if you would like to contribute. The assignment of di culty ratings is an on-going process. As part of this, we are collecting performance data for state-of-the-art theorem provers. TPTP users are invited to submit performance data for their ATP systems. Please contact us, or see the URL: for details if you would like to contribute. A BibTeX le will be added to the TPTP, containing entries for all the references found in the TPTP.

http://www.cs.jcu.edu.au.yzcaijing.com/~tptp/TPTP/Results.html

5.2 Further Plans

We have several short and long term plans for further development of the TPTP. The main ideas are listed here. ATP system evaluation guidelines. General guidelines outlining the requirements for ATP system evaluation will be produced. The BSTP Benchmark Suite. A benchmark suite (the BSTP) will be selected from the TPTP. The BSTP will be a small collection of problems, and will be a minimal set of problems on which an ATP system evaluation can be based. The BSTP will be accompanied by speci c guidelines for computing a performance index for an ATP system. Various translators. Translators between various logical forms will be provided. { from non-Horn to Horn form { from 1st order to propositional form 43

Other logics. The TPTP may be extended to include problems expressed in non-classical and higher order logics.

5.3 Acknowledgements

We are indebted to the following people and organizations who have helped with the construction of the TPTP. For contributing problems: Argonne National Labs, AR Research Group at TU Munchen, Bill McCune, Dan Benanav, Woody Bledsoe, Christian Fermuller, Thomas Jech, David Plaisted, Art Quaife, Alberto Segre, Stefan Schulz, John Slaney, Mark Stickel, Tanel Tammet, Bob Vero . For helping with problems and/or pointing out errors: Geo Alexander, Bill McCune, Woody Bledsoe, Maria Poala Bonacina, Heng Chu, Ingo Dahn, Matthias Fuchs, Tim Geisler, John Harrison, Thomas Jech, Harald Ganzinger, Reinhold Letz, Thomas Ludwig, Klaus Mayr, Xumin Nie, Je Pelletier, Art Quaife, Dimitris Raptis, Piotr Rudnicki, Len Schubert, Alberto Segre, John Slaney, Mark Stickel, Bob Vero , TC Wang, Christoph Weidenbach, Hantao Zhang. For support regarding the utilities: Max Moser, Gerd Neugebauer, Paul Tarau, Abdul Sattar, Christoph Weidenbach. For general advice and comments: Reiner Hahnle, Reinhold Letz, Mark Stickel.

References

Ada82] I. Adamson. Introduction to Field Theory. Cambridge University Press, 1982. AKPT91] J.F. Allen, H.A. Kautz, R.N. Pelavin, and J.D. Tenenberg. Reasoning about Plans. Morgan Kaufmann Publishers, 1991. ANL] ANL. Argonne National Laboratory Problem Library. Available by anonymous ftp from info.msc.anl.gov, Maths and Computer Science Division, Argonne National Laboratory, Argonne, IL. Ast94] O.L. Astrachan. METEOR: Exploring Model Elimination Theorem Proving. Journal of Automated Reasoning, 13(3):283{296, 1994. Bar81] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. NorthHolland, 1981. BB70] G. Birkho and T. Bartee. Modern Applied Algebra. McGraw-Hill, 1970. BL85] R.J. Brachman and H.J. Levesque. Readings in Knowledge Representation. Kaufmann Publishers, 1985. Ble90] W.W. Bledsoe. Challenge Problems in Elementary Calculus. Journal of Automated Reasoning, 6:341{359, 1990.

44

R. Boyer, E. Lusk, W.W. McCune, R. Overbeek, M. Stickel, and L. Wos. Set Theory in First-Order Logic: Clauses for Godel's Axioms. Journal of Automated Reasoning, 2(3):287{327, 1986. BM65] G. Birkho and S. MacLane. A Survey of Modern Algebra. Macmillan, 1965. Bou89] N. Bourbaki. Algebra I { Chapters 1-3. Springer Verlag, 1989. BP95] B. Beckert and J. Posegga. leanTAP: Lean, Tableau-based Deduction. Journal of Automated Reasoning, 15(3):339{358, 1995. Bun83] A. Bundy. The Computer Modelling of Mathematical Reasoning. Academic Press, 1983. Car86] L. Carroll. Lewis Carroll's Symbolic Logic. C.N. Potter, 1986. CF58] H.B. Curry and R. Feys. Combinatory Logic I. North Holland, Amsterdam, 1958. CHS72] H.B. Curry, J.R. Hindley, and J.P. Seldin. Combinatory Logic II. North Holland, Amsterdam, 1972. Chu56] A. Church. Introduction to Mathematical Logic I. Princeton University Press, 1956. Chu94] H. Chu. CLIN-S User's Manual. Chapel Hill, USA, 1994. CM87] N. Cercone and G. McCalla. The Knowledge Frontier : Essays in the Representation of Knowledge. Springer-Verlag, 1987. CP94] H. Chu and D. Plaisted. Semantically Guided First-order Theorem Proving using Hyper-linking. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, number 814 in Lecture Notes in Arti cial Intelligence, pages 192{206. Springer-Verlag, 1994. Dew89] M. Dewey. Dewey Decimal Classi cation and Relative Index. Forest Press, 20 edition, 1989. DGH+ 95] I.B. Dahn, J. Gehne, T. Honigmann, L. Walther, and A. Wolf. Integrating Logical Functions with ILF. Technical report, Institut fur Mathematik, Humboldt Universitat zu Berlin, Berlin, Germany, 1995. DIM] DIMACS. Satis ability Suggested Format. ftp://dimacs.rutgers.edu/ pub/challenge/satis ability/doc/satformat.tex. Dra93] J. Draeger. Anwendung des Theorembeweisers SETHEO auf angeordnete Korper. Technical Report Technical Report FKI-186-93, Technische Universitat Munchen, Munchen, Germany, 1993. FHKF92] M. Fujita, R. Hasegawa, M. Koshimura, and H. Fujita. Model Generation Theorem Provers on a Parallel Inference Machine. In Proceedings of the International Conference on Fifth Generation Computer Systems, pages 357{ 375, 1992. 45

BLM+ 86]

GF92] Har69] Hay93] HBG94] Hen50] HKW96] HMT71] How72] HU79] HW92] Jec93] Kel55] Leb83] LM92] LSBB92] Luk63] Mac71]

M.R. Genesereth and R.E. Fikes. Knowledge Interchange Format, Version 3.0 Reference Manual. Technical Report Technical Report Logic-92-1, Computer Science Department, Stanford University, 1992. F. Harary. Graph Theory. Addison-Wesley, 1969. J.P. Hayes. Introduction to Digital Logic Circuit Design. Addison Wesley, 1993. R. Hahnle, B. Beckert, and S. Gerberding. The Many-Valued Tableau-Based Theorem Prover 3TAP. Technical Report TR 30/94, Fakultat fur Informatik, Universat Karlsruhe, Karlsruhe, Germany, 1994. L. Henkin. Completeness in the Theory of Types. Journal of Symbolic Logic, 15:81{91, 1950. R. Hahnle, M. Kerber, and C. Weidenbach. Common Syntax of the DFGSchwerpunktprogramm Deduction. Technical Report TR 10/96, Fakultat fur Informatik, Universat Karlsruhe, Karlsruhe, Germany, 1996. L. Henkin, J. Monk, and A. Tarski. Cylindrical Algebras, volume Part 1. North-Holland, 1971. A.G. Howson. A Handbook of Terms used in Algebra and Analysis. Cambrige University Press, 1972. J. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, 1979. G.H. Hardy and E.M. Wright. An Introduction to the Theory of Numbers. Oxford UP, 5 edition, 1992. T. Jech. LD-algebras. Association for Automated Reasoning Newsletter, 22:9{12, 1993. J.L. Kelley. General Topology. D. Van Nostrand, 1955. H. Leblanc. Alternatives to Standard First-Oder Semantics. In D. Gabbay and F. Guenther, editors, Handbook of Philosophical Logic, volume I, chapter I.3, pages 189{274. D. Reidel, 1983. E.L. Lusk and W.W. McCune. Experiments with ROO, a Parallel Automated Deduction System. In B. Fronhofer and G. Wrightson, editors, Parallelization in Inference Systems, volume 590, pages 139{162, 1992. R. Letz, J. Schumann, S. Bayerl, and W. Bibel. SETHEO: A HighPerformance Theorem Prover. Journal of Automated Reasoning, 8(2):183{ 212, 1992. J. Lukasiewicz. Elements of Mathematical Logic. Pergamon Press, 1963. S. MacLane. Categories for the Working Mathematician. Springer Verlag, 1971. 46

McC88]

W. McCune. Challenge Equality Problems in Lattice Theory. In Proceedings of the 9th International Conference on Automated Deduction - Argonne Ilinois, USA, May 1988, pages 704 { 709, Berlin, 1988. Springer. McC90] W.W. McCune. Equality in Automated Deduction. In Swartout W. Dietterich T., editor, Proceedings of the 8th National Conference on Arti cial Intelligence , pages 246{252. American Association for Arti cial Intelligence / MIT Press, 1990. McC93] W.W. McCune. Single Axioms for Groups and Abelian Groups with Various Operations. Journal of Automated Reasoning, 10(1):1{13, 1993. McC94] W.W. McCune. Otter 3.0 Reference Manual and Guide. Technical Report Technical Report ANL-94/6, Argonne National Laboratory, Argonne, USA, 1994. MOW76] J.D. McCharen, R.A. Overbeek, and L.A. Wos. Problems and Experiments for and with Automated Theorem-Proving Programs. IEEE Transactions on Computers, C-25(8):773{782, 1976. MSC92] Mathematical Subject Classi cation. American Mathematical Society, Provedence, USA, 1992. Mun75] J.R. Munkres. Topology: A First Course. Prentice-Hall, 1975. MW92] W. McCune and L. Wos. Experiments in Automated Deduction with Condensed Detachment. In Kapur D., editor, Proceedings of the 11th International Conference on Automated Deduction , number 607 in Lecture Notes in Arti cial Intelligence, pages 209{223. Springer-Verlag, 1992. Neu25] J. von Neumann. Eine Axiomatisierung der Mengenlehre. Journal fur die reine und angewandte Mathematik, 154:219{240, 1925. PBMON94] G. Peli, J. Bruggeman, M. Masuch, and B. O Nuallain. A Logical Approach to Formalizing Organizational Ecology: Formalizing the Inertia-Fragment in First-Order Logic. American Sociological Review, 59(2), 1994. Pel86] F.J. Pelletier. Seventy- ve Problems for Testing Automatic Theorem Provers. Journal of Automated Reasoning, 2(2):191{216, 1986. Pla81] D.A. Plaisted. Theorem Proving with Abstraction. Arti cial Intelligence, 16:47{108, 1981. Pla82] D.A. Plaisted. A Simpli ed Problem Reduction Format. Arti cial Intelligence, 18:227{261, 1982. Pla88] D.A. Plaisted. Non-Horn Clause Logic Programming Without Contrapositives. Journal of Automated Reasoning, 4(3):287{325, 1988. PM94] G. Peli and M. Masuch. The Logic of Propogation Strategies: Axiomatizing a Fragment of Organization Ecology in First-Order Logic. In D.P. Moore, editor, Academy Of Management: Best Papers Proceedings 1994, pages 218{ 222, Dallas, USA, 1994. 47

J.L. Pollock. Interest Driven Suppositional Reasoning. Journal of Automated Reasoning, 6(4):419{461, 1990. Qua90] A. Quaife. Email to G. Sutcli e. 1990. Qua92a] A. Quaife. Automated Deduction in von Neumann-Bernays-Godel Set Theory. Journal of Automated Reasoning, 8(1):91{147, 1992. Qua92b] A. Quaife. Automated Development of Fundamental Mathematical Theories. Kluwer Academic Publishers, 1992. Qua92c] A. Quaife. Email to G. Sutcli e. 1992. Qui69] W.V. Quine. Set Theory and its Logic. Harvard University Press, 1969. Ros90] K.A. Ross. Elementary Analysis: The Theory of Calculus. Springer, 2nd edition, 1990. SM96] G. Sutcli e and S. Melville. The Practice of Clausi cation in Automatic Theorem Proving. South African Computer Journal, 18:57{68, 1996. Smu78a] R.M. Smullyan. To Mock a Mocking Bird and Other Logic Puzzles. Knopf, 1978. Smu78b] R.M. Smullyan. What is the name of this book?-The riddle of Dracula and other logical puzzles. Prentice-Hall, 1978. SPR] SPRFN. The problem collection distributed with the SPRFN ATP system. SS96] C.B. Suttner and G. Sutcli e. The TPTP Problem Library (TPTP v2.0.0), 1996. Technical Report AR-97-ZZ, Institut fur Informatik, Technische Universitat Munchen, Munich, Germany; Technical Report 97/ZZ, Department of Computer Science, James Cook University, Townsville, Australia. Sti84] M.E. Stickel. A Prolog Technology Theorem Prover. New Generation Computing, 2(4):371{383, 1984. Sti86] M.E. Stickel. Schubert's Steamroller Problem: Formulations and Solutions. Journal of Automated Reasoning, 2(1):89{101, 1986. Sti94] M.E. Stickel. Upside-Down Meta-Interpretation of the Model Elimination Theorem-Proving Procedure for Deduction and Abduction. Journal of Automated Reasoning, 13(2):189{210, 1994. STvdK90] J. Schumann, N. Trapp, and M. van der Koelen. SETHEO/PARTHEO Users Manual. Technical Report SFB Bericht 342/7/90 A, Institut fur Informatik, Technische Universitat Munchen, Munich, Germany, 1990. Tar51] A. Tarski. A Decision Method for Elementary Algebra and Geometry. University of California Press, 2ed edition, 1951. Tar59] A. Tarski. What is Elementary Geometry? In L. Henkin, editor, Proceedings of an International Symposium. The axiomatic method with special reference to geometry and physics. North-Holland, 1959. 48

Pol90]

J.E. Whitesitt. Boolean Algebra and Its Applications. Addison-Wesley, 1961. S. Winker. Robbins Algebra: Conditions that make a Near-Boolean Algebra Boolean. Journal of Automated Reasoning, 6(4):465{489, 1990. WM76] G.A. Wilson and J. Minker. Resolution Strategies: A Comparative Study. IEEE Transactions on Computers, C-25(8):782{801, 1976. WM88] L. Wos and W. McCune. Challenge Problems Focusing on Equality and Combinatory Logic: Evaluating Automated Theorem-Proving Programs. In Overbeek R. Lusk E., editor, Proceedings of the 9th International Conference on Automated Deduction , number 310 in Lecture Notes in Computer Science, pages 714{729. Springer-Verlag, 1988. WM89] C. Wick and W. McCune. Automated Reasoning about Elementary PointSet Topology. Journal of Automated Reasoning, 5:239 { 255, 1989. Woj83] A.S. Wojcik. Formal Design Veri cation of Digital Systems. In Proceedings of the 20th Design Automation Conference, 1983. WOLB92] L. Wos, R. Overbeek, E. Lusk, and J. Boyle. Automated Reasoning: Introduction and Applications. Prentice-Hall, 2nd edition, 1992. WW83] W.S. Wojciechowski and A.S. Wojcik. Automated Design of Multi-valued Logic Circuits by Automated Theorem Proving Techniques. IEEE Transactions on Computers, C-32(8):785{798, 1983.

Whi61] Win90]

49