TPTP Organization

TPTP Physical Organization
- Axioms directory - Axiom files, which are included into problem files
  - Browsing interface
- Problems directory - Domain directories - Problem files
  - Browsing interface
- Generators directory - Generator code files
- Documents directory - Documentation files
  - Browsing interface
- Scripts directory - Utility scripts
- TPTP2X directory - The TPTP2X utility

Domain Structure

Reflects natural hierarchy of scientific domains
Based on the DDC and MSC classification schemes

Fields - Domains - Mnemonics - Problems

Field Domain Mnemonic Problems FOF CNF

Logic Combinatory Logic COL 239 0 239
Logic Calculi LCL 702 136 566
Henkin Models HEN 67 0 67

Mathematics Set Theory SET 1268 468 800
Set Theory Continued SEU 906 906 0
Graph Theory GRA 33 32 1
Algebras
    Boolean Algebra BOO 140 1 139
    Robbins Algebra ROB 40 0 40
    Left Distributive LDA 23 0 23
    Lattices LAT 707 397 310
    Groups GRP 941 149 792
    Rings RNG 104 0 104
    Fields FLD 279 0 279
    Homological Alg HAL 9 9 0
    General Algebra ALG 300 285 15
Number Theory NUM 451 136 315
Topology TOP 131 107 24
Analysis ANA 91 0 91
Geometry GEO 489 236 253
Category Theory CAT 130 68 62

Computer Science Computing Theory COM 21 7 14
Knowledge Representation KRS 175 158 17
Natural Language Processing NLP 516 258 258
Planning PLA 46 6 40
Agents AGT 52 52 0
Commonsense Reasoning CSR 442 442 0
Software Creation SWC 846 423 423
Software Verification SWV 630 288 342

Science & Engg Hardware Creation HWC 6 0 6
Hardware Verification HWV 83 0 83
Medicine MED 10 10 0

Social Sciences Management MGT 156 78 78

Other Syntactic SYN 1208 366 842
Puzzles PUZ 126 24 102
Miscellaneous MSC 28 7 21

Problem Versions
- Abstract problems
- Problem versions
  - Different formulations
  - Different axiomatizations
    - Standard axiomatizations - complete for an established theory
    - Non-standard axiomatizations - modified standard axiomatizations
    - Especial axiomatizations
  - Different sizes
File Naming
- Provides stable, unambiguous names for problems, axiomatizations, and generators
- Problem file names of the form DDDNNNFV[.SSS].p
  - DDD - Domain name mnemonic
  - NNN - Abstract problem number
  - F - Form, + for FOF, - for CNF
  - V - Version number
  - SSS - Size parameter(s) for generated files
  - .p - File name extension, p for problem files
- Axiom file names of the form DDDNNNFS.ax
  - DDD - Domain name mnemonic
  - NNN - Axiomatization number
  - S - Specialization number, 0 for base theories, 1 onwards for specializations
  - .ax - File name extension, ax for axiom files
- Generator file names of the form DDDNNNFV.g, ala problem files
- DDDNNN names an abstract problem or axiomatization
- DDDNNNFV[.SSS] names a problem or generator
- DDDNNNFS names a set of axioms
- If a file is ever "removed" the extension is changed to .rm

Field	Domain	Mnemonic	Problems	FOF	CNF

Logic	Combinatory Logic	`COL`	239	0	239
	Logic Calculi	`LCL`	702	136	566
	Henkin Models	`HEN`	67	0	67

Mathematics	Set Theory	`SET`	1268	468	800
	Set Theory Continued	`SEU`	906	906	0
	Graph Theory	`GRA`	33	32	1
	Algebras
	Boolean Algebra	`BOO`	140	1	139
	Robbins Algebra	`ROB`	40	0	40
	Left Distributive	`LDA`	23	0	23
	Lattices	`LAT`	707	397	310
	Groups	`GRP`	941	149	792
	Rings	`RNG`	104	0	104
	Fields	`FLD`	279	0	279
	Homological Alg	`HAL`	9	9	0
	General Algebra	`ALG`	300	285	15
	Number Theory	`NUM`	451	136	315
	Topology	`TOP`	131	107	24
	Analysis	`ANA`	91	0	91
	Geometry	`GEO`	489	236	253
	Category Theory	`CAT`	130	68	62

Computer Science	Computing Theory	`COM`	21	7	14
	Knowledge Representation	`KRS`	175	158	17
	Natural Language Processing	`NLP`	516	258	258
	Planning	`PLA`	46	6	40
	Agents	`AGT`	52	52	0
	Commonsense Reasoning	`CSR`	442	442	0
	Software Creation	`SWC`	846	423	423
	Software Verification	`SWV`	630	288	342

Science & Engg	Hardware Creation	`HWC`	6	0	6
	Hardware Verification	`HWV`	83	0	83
	Medicine	`MED`	10	10	0

Social Sciences	Management	`MGT`	156	78	78

Other	Syntactic	`SYN`	1208	366	842
	Puzzles	`PUZ`	126	24	102
	Miscellaneous	`MSC`	28	7	21